Removed the ssreflect dependency and fixed some "Admitted"

liouville/CPoly_Euclid.v

@@ -52,8 +52,7 @@ Theorem cpoly_div1 : forall (m n : nat) (f g : cpoly_cring CR),
     let (q,r):=qr in f [*] _C_ ((nth_coeff (S n) g) [^] (m - n)) [=] q [*] g [+] r &
     let (q,r):=qr in degree_le n r}.
 Proof.
-Admitted. (*
- intros m n; set (H := refl_equal (m - n)); revert H.
+ intros m n; generalize (refl_equal (m - n)).
  generalize (m - n) at 1 as p; intro p; revert m n; induction p; intros.
   exists (([0] : cpoly_cring CR),f).
    rewrite <- H.
@@ -72,28 +71,26 @@ Admitted. (*
  replace (m - 1 - n) with (m - S n) by omega.
  rewrite <- nexp_Sn.
  generalize (nth_coeff (S n) g) (nth_coeff m f) (m - S n).
- intros. rewrite c_mult c_mult. unfold cg_minus. ring.
+ intros. rewrite c_mult, c_mult. unfold cg_minus. ring.
 Qed.
-*)
 
 Definition degree_lt_pair (p q : cpoly_cring CR) := (forall n : nat, degree_le (S n) q -> degree_le n p) and (degree_le O q -> p [=] [0]).
 Lemma cpoly_div2 : forall (n m : nat) (a b c : cpoly_cring CR),
   degree_le n a -> monic m b -> degree_lt_pair c b -> a [*] b [=] c ->
     a [=] [0].
 Proof.
-Admitted. (*
  induction n.
   intros m a b c H X H1 H2; destruct (degree_le_zero _ _ H) as [x s].
-  move: H1. rewrite -> s; destruct X as [H0 H1]; rewrite -> c_zero. rewrite -> s in H2. intro. apply cpoly_const_eq.
+  revert H1. rewrite -> s; destruct X as [H0 H1]; rewrite -> c_zero. rewrite -> s in H2. intro. apply cpoly_const_eq.
   destruct m.
-   set (tmp := nth_coeff_wd _ 0 _ _ H2); destruct H3 as [d s0].
-   move: tmp. rewrite -> nth_coeff_c_mult_p, H0, mult_one, (nth_coeff_wd _ _ _ _ (s0 H1)). intro tmp; apply tmp.
-   set (tmp := nth_coeff_wd _ (S m) _ _ H2); destruct H3 as [d s0].
-  move: tmp. rewrite -> nth_coeff_c_mult_p, H0, mult_one, (d m H1 (S m)).  apply. apply le_n.
+   generalize (nth_coeff_wd _ 0 _ _ H2); destruct H3 as [d s0].
+   rewrite -> nth_coeff_c_mult_p, H0, mult_one, (nth_coeff_wd _ _ _ _ (s0 H1)). intro tmp; apply tmp.
+   generalize (nth_coeff_wd _ (S m) _ _ H2); destruct H3 as [d s0].
+  rewrite -> nth_coeff_c_mult_p, H0, mult_one, (d m H1 (S m)).  intro; assumption. apply le_n.
   intros.
  induction a as [ | a s ] using cpoly_induc; [ reflexivity | ].
  apply _linear_eq_zero.
- move: H2. rewrite -> cpoly_lin, ring_distl_unfolded. intro H2.
+ revert H2. rewrite -> cpoly_lin, ring_distl_unfolded. intro H2.
  cut (a [=] [0]); [ intro aeqz; split; [ | apply aeqz ] | ].
   assert (s [=] nth_coeff m (_C_ s[*]b[+]_X_[*]a[*]b)).
    destruct H0; rewrite -> nth_coeff_plus, nth_coeff_c_mult_p, H0.
@@ -118,11 +115,10 @@ Admitted. (*
   destruct m; [ destruct H0; apply (nth_coeff_wd _ _ _ _ (s0 H1)) | ].
   apply (d n0); [ | apply H4 ].
   apply (degree_le_mon _ _ n0); [ apply le_S; apply le_n | apply (degree_le_cpoly_linear _ _ _ _ H3) ].
- destruct (degree_le_zero _ _ H3) as [x s0]. move: s0. rewrite -> cpoly_C_. intro s0.
+ destruct (degree_le_zero _ _ H3) as [x s0]. revert s0. rewrite -> cpoly_C_. intro s0.
  destruct (linear_eq_linear_ _ _ _ _ _ s0) as [H4 H5].
  rewrite <- H2, -> H5. unfold cg_minus. ring.
 Qed.
-*)
 
 Lemma cpoly_div : forall (f g : cpoly_cring CR) (n : nat), monic n g ->
   ex_unq (fun (qr : ProdCSetoid (cpoly_cring CR) (cpoly_cring CR)) => f[=](fst qr)[*]g[+](snd qr) and degree_lt_pair (snd qr) g).

liouville/QX_ZX.v

@@ -23,7 +23,6 @@ Require Import CoRN.model.rings.Qring.
 Require Import Zring.
 Require Import Qordfield.
 Require Import CRing_Homomorphisms.
-Require Import ssreflect.
 
 Require Import RingClass CRingClass.
 Require Import Zlcm Q_can RX_deg.
@@ -146,16 +145,16 @@ Proof.
   cut (Zpos Qden = Zgcd Qnum Qden).
    intro H0; rewrite H0.
    apply Zgcd_is_divisor_lft.
-  rewrite {1} (Zgcd_div_mult_rht Qnum Qden).
-   intro.
-   destruct (Zgcd_zero _ _ H0).
-   rewrite H1 in H.
-   rewrite H2 in H.
-   rewrite Zgcd_zero_rht in H.
-   rewrite Zdiv_0_r in H.
-   discriminate.
-  rewrite H.
-  apply Zmult_1_l.
+  rewrite (Zgcd_div_mult_rht Qnum Qden) at 1.
+   rewrite H.
+   apply Zmult_1_l.
+  intro.
+  destruct (Zgcd_zero _ _ H0).
+  rewrite H1 in H.
+  rewrite H2 in H.
+  rewrite Zgcd_zero_rht in H.
+  rewrite Zdiv_0_r in H.
+  discriminate.
  unfold Q_can_den.
  destruct q; simpl in *.
  case (Z_dec Qnum 0).
@@ -165,7 +164,7 @@ Proof.
   discriminate.
  intro Hap.
  cut (Zpos Qden = Zgcd Qnum Qden).
-  intro H0; rewrite {1} H0.
+  intro H0; rewrite H0 at 1.
   apply Z_div_same_full.
   intro H1; destruct (Zgcd_zero _ _ H1).
   discriminate.
@@ -197,13 +196,13 @@ Proof.
   destruct (zero_eq_linear_ _ _ _ Heq).
   split.
    rewrite (Q_can_num_spec _ [0]).
-    assumption.
-   reflexivity.
+    reflexivity.
+   assumption.
   change ([0] [=] Q_can_num_poly P).
   symmetry; apply Hrec; symmetry; assumption.
  intros P Q c d Hrec Heq.
  destruct (linear_eq_linear_ _ _ _ _ _ Heq).
- rewrite Q_can_num_poly_linear Q_can_num_poly_linear.
+ rewrite Q_can_num_poly_linear, Q_can_num_poly_linear.
  apply _linear_eq_linear.
  split.
   apply Q_can_num_spec; assumption.
@@ -245,9 +244,9 @@ Proof.
   unfold Q_can_num; simpl; unfold Qeq; simpl.
   rewrite Zmult_1_r.
   intro H; rewrite (Zgcd_div_mult_lft qn qd).
-   intro H0; destruct (Zgcd_zero _ _ H0); discriminate.
-  rewrite H.
-  apply Zmult_0_l.
+   rewrite H.
+   apply Zmult_0_l.
+  intro H0; destruct (Zgcd_zero _ _ H0); discriminate.
  reflexivity.
 Qed.
 
@@ -269,7 +268,7 @@ Lemma injZ_strext : fun_strext (inject_Z : Z_as_CRing -> Q_as_CRing).
 Proof.
  intros x y.
  unfold inject_Z; simpl; unfold Qap, Qeq, ap_Z; simpl.
- rewrite Zmult_1_r Zmult_1_r; tauto.
+ rewrite Zmult_1_r, Zmult_1_r; tauto.
 Qed.
 Lemma injZ_spec : forall q : Q_as_CRing, in_Z q -> q [=] (Q_can_num q).
 Proof.
@@ -283,19 +282,19 @@ Proof.
  unfold Q_can_den in Hin.
  simpl in Hin.
  cut (Zpos qd = Zgcd qn qd).
-  intro H; rewrite {2} H.
+  intro H; rewrite H at 2.
   rewrite Zmult_comm.
   symmetry; apply Zdivides_spec.
   apply Zgcd_is_divisor_lft.
- rewrite {1} (Zgcd_div_mult_rht qn qd).
-  intro H; destruct (Zgcd_zero _ _ H); discriminate.
- rewrite Hin; rewrite Zmult_1_l; reflexivity.
+ rewrite (Zgcd_div_mult_rht qn qd) at 1.
+  rewrite Hin; rewrite Zmult_1_l; reflexivity.
+ intro H; destruct (Zgcd_zero _ _ H); discriminate.
 Qed.
 Lemma injZ_spec2 : forall p : Z_as_CRing, p = Q_can_num p.
 Proof.
  intro p.
  unfold Q_can_num, inject_Z; simpl.
- rewrite Zgcd_one_rht Zdiv_1_r; reflexivity.
+ rewrite Zgcd_one_rht, Zdiv_1_r; reflexivity.
 Qed.
 Definition injZ_fun := Build_CSetoid_fun _ _ _ injZ_strext.
 
@@ -345,7 +344,7 @@ Proof.
  rewrite -> nth_coeff_zx2qx.
  rewrite -> (injZ_spec _ i).
  unfold inject_Z; simpl; unfold Qeq; simpl.
- rewrite Zmult_1_r Zmult_1_r.
+ rewrite Zmult_1_r, Zmult_1_r.
  symmetry; apply nth_coeff_Q_can_num_poly_spec.
 Qed.
 

liouville/QX_extract_roots.v

@@ -23,7 +23,6 @@ Require Import CRing_Homomorphisms.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CauchySeq.
 Require Import Q_in_CReals.
-Require Import ssreflect.
 
 Require Import CPoly_Euclid RingClass CRingClass.
 Require Import Q_can nat_Q_lists RX_deg RX_div QX_root_loc.
@@ -169,21 +168,21 @@ Proof.
  revert Heq.
  unfold QX_deg; rewrite (RX_deg_wd _ Q_dec _ _ (RX_div_spec _ p a)).
  rewrite RX_deg_sum.
-  rewrite RX_deg_c_.
+  rewrite max_comm.
   rewrite -> QX_deg_mult.
     unfold QX_deg; rewrite RX_deg_minus.
-     rewrite RX_deg_x_ RX_deg_c_; discriminate.
-    rewrite RX_deg_x_ RX_deg_c_.
-    rewrite plus_comm; discriminate.
+     rewrite RX_deg_c_, RX_deg_x_, RX_deg_c_; fold QX_deg.
+     simpl; rewrite plus_comm; simpl.
+     intro H; injection H; symmetry; assumption.
+    rewrite RX_deg_x_, RX_deg_c_; discriminate.
    apply QX_div_deg0; assumption.
   right; left; discriminate.
- rewrite max_comm.
+ rewrite RX_deg_c_.
  rewrite -> QX_deg_mult.
    unfold QX_deg; rewrite RX_deg_minus.
-    rewrite RX_deg_x_ RX_deg_c_; discriminate.
-   rewrite RX_deg_c_ RX_deg_x_ RX_deg_c_; fold QX_deg.
-   simpl; rewrite plus_comm; simpl.
-   intro H; injection H; symmetry; assumption.
+    rewrite RX_deg_x_, RX_deg_c_.
+    rewrite plus_comm; discriminate.
+   rewrite RX_deg_x_, RX_deg_c_; discriminate.
   apply QX_div_deg0; assumption.
  right; left; discriminate.
 Qed.

liouville/QX_root_loc.v

@@ -23,7 +23,6 @@ Require Import CRing_Homomorphisms.
 Require Import Qring.
 Require Import Zring.
 Require Import Qordfield.
-Require Import ssreflect.
 
 Require Import RingClass CRingClass.
 Require Import Zlcm Q_can nat_Q_lists RX_deg QX_ZX.
@@ -83,7 +82,7 @@ Proof.
  apply (mult_wdr _ (inject_Z ((p:Z_as_CRing)[^]i)) ((q:Q_as_CRing)[*](p # q)%Q) p).
  simpl; unfold Qeq; simpl.
  case p.
-   rewrite Zmult_0_l Zmult_0_l; reflexivity.
+   rewrite Zmult_0_l, Zmult_0_l; reflexivity.
   intro r; rewrite Zmult_1_r; rewrite Zmult_comm; reflexivity.
  intro r; rewrite Zmult_1_r; rewrite Zmult_comm; reflexivity.
 Qed.
@@ -118,7 +117,7 @@ Proof.
  rewrite -> nexp_ring_hom, nexp_ring_hom.
  rewrite <- CRings.mult_assoc, <- CRings.mult_assoc.
  apply mult_wdr.
- rewrite {1} (le_plus_minus _ _ Hn).
+ rewrite (le_plus_minus _ _ Hn) at 1.
  clear H0 Hn.
  rewrite <- nexp_plus.
  rewrite -> CRings.mult_assoc.
@@ -222,7 +221,7 @@ Proof.
  assert (Q_can_num ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q) [=] [0]).
   rewrite (Q_can_num_spec _ _ H).
   unfold Q_can_num; simpl.
-  rewrite Zgcd_one_rht Zdiv_0_l; reflexivity.
+  rewrite Zgcd_one_rht, Zdiv_0_l; reflexivity.
  clear Hval H; revert H0.
  rewrite (Q_can_num_spec _ _ (Q_Z_poly_apply _ _ _)).
  rewrite <- injZ_spec2.
@@ -325,7 +324,7 @@ Proof.
  assert (Q_can_num ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q) [=] [0]).
   rewrite (Q_can_num_spec _ _ H).
   unfold Q_can_num; simpl.
-  rewrite Zgcd_one_rht Zdiv_0_l; reflexivity.
+  rewrite Zgcd_one_rht, Zdiv_0_l; reflexivity.
  clear Hval H; revert H0.
  rewrite (Q_can_num_spec _ _ (Q_Z_poly_apply _ _ _)).
  rewrite <- injZ_spec2.

liouville/Q_can.v

@@ -20,7 +20,6 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
 Require Import CRings Qring Zring.
-Require Import ssreflect.
 Require Import Zlcm.
 
 Section Q_can.
@@ -44,11 +43,11 @@ Proof.
  rewrite -> (Zmult_comm (Zgcd q'n q'd) (q'n / Zgcd q'n q'd)).
  rewrite <- Zgcd_div_mult_lft, <- Zgcd_div_mult_lft;
    try (intro H; destruct (Zgcd_zero _ _ H); discriminate).
- rewrite Zmult_comm (Zmult_comm _ q'n).
+ rewrite Zmult_comm, (Zmult_comm _ q'n).
  rewrite <- (Zabs_Zsgn qn) at 1; rewrite <- (Zabs_Zsgn q'n) at 2.
- rewrite (Zmult_comm (Zabs qn)) (Zmult_comm (Zabs q'n)).
+ rewrite (Zmult_comm (Zabs qn)), (Zmult_comm (Zabs q'n)).
  rewrite <- Zmult_assoc, <- Zmult_assoc.
- rewrite Zgcd_lin Zgcd_lin.
+ rewrite Zgcd_lin, Zgcd_lin.
  rewrite Heq.
  rewrite (Zmult_comm qn q'n).
  cut (Zsgn qn = Zsgn q'n).
@@ -73,12 +72,12 @@ Proof.
  rewrite (Zmult_comm (Zgcd q'n q'd) (q'd / Zgcd q'n q'd)).
  rewrite <- Zgcd_div_mult_rht, <- Zgcd_div_mult_rht;
    try (intro H; destruct (Zgcd_zero _ _ H); discriminate).
- rewrite Zmult_comm (Zmult_comm _ q'd).
+ rewrite Zmult_comm, (Zmult_comm _ q'd).
  rewrite <- (Zabs_Zsgn qd) at 1; rewrite <- (Zabs_Zsgn q'd) at 2.
- rewrite (Zmult_comm (Zabs qd)) (Zmult_comm (Zabs q'd)).
+ rewrite (Zmult_comm (Zabs qd)), (Zmult_comm (Zabs q'd)).
  rewrite <- Zmult_assoc, <- Zmult_assoc.
- rewrite Zgcd_lin Zgcd_lin.
- rewrite (Zmult_comm qd q'n) (Zmult_comm q'd qn).
+ rewrite Zgcd_lin, Zgcd_lin.
+ rewrite (Zmult_comm qd q'n), (Zmult_comm q'd qn).
  rewrite Heq.
  rewrite (Zmult_comm qd q'd).
  reflexivity.
@@ -93,7 +92,7 @@ Proof.
  assert (0 < Zgcd qn qd)%Z.
   apply Zgcd_pos; right; discriminate.
  assert (Zgcd qn qd <= qd)%Z.
-  by apply Zgcd_le_rht.
+  apply Zgcd_le_rht; apply Zgt_pos_0.
  apply Z.div_str_pos.
  split; assumption.
 Qed.

liouville/RX_deg.v

@@ -19,7 +19,6 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 Require Import CPoly_Degree RingClass CRingClass.
-Require Import ssreflect.
 
 Section RX_deg.
 
@@ -151,7 +150,7 @@ Lemma RX_deg_inv : forall p, RX_deg p = RX_deg ([--]p).
 Proof.
  intro p.
  case (RX_dec p [0]).
-  intro H; rewrite (RX_deg_wd _ _ H) RX_deg_zero.
+  intro H; rewrite (RX_deg_wd _ _ H), RX_deg_zero.
   rewrite <- RX_deg_zero; apply RX_deg_wd; rewrite -> H; unfold RX; ring.
  intro Hp.
  apply (degree_inj p).
@@ -177,27 +176,27 @@ Proof.
  set (RX_deg_spec _ Hp).
  set (RX_deg_spec _ Hq).
  case (le_lt_dec (RX_deg p) (RX_deg q)); intro.
-  rewrite max_r; [assumption|].
+  rewrite max_r; [|assumption].
   inversion l.
    destruct (Hneq H0).
   apply (degree_inj (p[+]q)).
    apply RX_deg_spec.
    case (RX_dec (p[+]q) [0]); [|tauto].
    intro; destruct Hneq.
    rewrite (RX_deg_wd p ([--]q)).
-    apply cg_inv_unique'; assumption.
-   symmetry; apply RX_deg_inv.
+    symmetry; apply RX_deg_inv.
+   apply cg_inv_unique'; assumption.
   apply (degree_plus_rht _ _ _ m); [| |apply le_n].
    apply (degree_le_mon _ _ (RX_deg p)); [assumption|apply d].
   rewrite H; apply RX_deg_spec; assumption.
- rewrite max_l; [apply lt_le_weak; assumption|].
+ rewrite max_l; [|apply lt_le_weak; assumption].
  apply (degree_inj (p[+]q)).
   apply RX_deg_spec.
   case (RX_dec (p[+]q) [0]); [|tauto].
   intro; destruct Hneq.
   rewrite (RX_deg_wd p ([--]q)).
-   apply cg_inv_unique'; assumption.
-  symmetry; apply RX_deg_inv.
+   symmetry; apply RX_deg_inv.
+  apply cg_inv_unique'; assumption.
  apply (degree_wd _ _ _ _ (cag_commutes _ _ _)).
  apply (degree_plus_rht _ _ _ (RX_deg q)); [| |assumption].
   apply degree_imp_degree_le.