Field_theory : faster and nicer proofs + nice notations.

 This file should compile now twice as fast as earlier.
 A large part of this speedup comes from swithching to
 proofs without "auto" (and also improving them quite a lot).

 Nicer lemma statements thanks to notations and
 separate scopes (%ring, %coef, %poly).

 The Field_correct lemma lost some args (sign_theory ...)
 during the refactoring. After inspection, this looks legitimate,
 so I've hack the field tactic accordingly. The args were there
 probably due to some intuition or similar interfering with local
 vars.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16721 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 1027 insertions, 1185 deletions

diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index 8ac952c04..c46e7a933 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -542,10 +542,9 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
          let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in
          match s_spec with
          | mkhypo ?ss_spec =>
-           let field_ok3 := constr:(field_ok2 _ ss_spec) in
            match d_spec with
            | mkhypo ?dd_spec =>
-             let field_ok := constr:(field_ok3 _ dd_spec) in
+             let field_ok := constr:(field_ok2 _ dd_spec) in
              let mk_lemma lemma :=
               constr:(lemma _ _ _  _ _ _  _ _ _ _
                    set ext_r inv_m afth
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 2f30b6e17..d584adfc8 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -9,118 +9,155 @@
 Require Ring.
 Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms.
 Require Import ZArith_base.
-(*Require Import Omega.*)
 Set Implicit Arguments.
 
 Section MakeFieldPol.
 
-(* Field elements *)
- Variable R:Type.
- Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
- Variable (rdiv : R -> R ->  R) (rinv : R ->  R).
- Variable req : R -> R -> Prop.
-
- Notation "0" := rO. Notation "1" := rI.
- Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
- Notation "x - y " := (rsub x y). Notation "x / y" := (rdiv x y).
- Notation "- x" := (ropp x). Notation "/ x" := (rinv x).
- Notation "x == y" := (req x y) (at level 70, no associativity).
-
- (* Equality properties *)
- Variable Rsth : Equivalence req.
- Variable Reqe : ring_eq_ext radd rmul ropp req.
- Variable SRinv_ext : forall p q, p == q ->  / p == / q.
-
- (* Field properties *)
-  Record almost_field_theory : Prop := mk_afield {
-    AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req;
-    AF_1_neq_0 : ~ 1 == 0;
-    AFdiv_def : forall p q, p / q == p * / q;
-    AFinv_l : forall p, ~ p == 0 ->  / p * p == 1
-  }.
+(* Field elements : R *)
+
+Variable R:Type.
+Bind Scope R_scope with R.
+Delimit Scope R_scope with ring.
+
+Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
+Variable (rdiv : R -> R ->  R) (rinv : R ->  R).
+Variable req : R -> R -> Prop.
+
+Notation "0" := rO : R_scope.
+Notation "1" := rI : R_scope.
+Infix "+" := radd : R_scope.
+Infix "-" := rsub : R_scope.
+Infix "*" := rmul : R_scope.
+Infix "/" := rdiv : R_scope.
+Notation "- x" := (ropp x) : R_scope.
+Notation "/ x" := (rinv x) : R_scope.
+Infix "==" := req (at level 70, no associativity) : R_scope.
+
+Local Open Scope R_scope.
+
+(* Equality properties *)
+Variable Rsth : Equivalence req.
+Variable Reqe : ring_eq_ext radd rmul ropp req.
+Variable SRinv_ext : forall p q, p == q ->  / p == / q.
+
+(* Field properties *)
+Record almost_field_theory : Prop := mk_afield {
+ AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req;
+ AF_1_neq_0 : ~ 1 == 0;
+ AFdiv_def : forall p q, p / q == p * / q;
+ AFinv_l : forall p, ~ p == 0 ->  / p * p == 1
+}.
 
 Section AlmostField.
 
- Variable AFth : almost_field_theory.
- Let ARth := AFth.(AF_AR).
- Let rI_neq_rO := AFth.(AF_1_neq_0).
- Let rdiv_def := AFth.(AFdiv_def).
- Let rinv_l := AFth.(AFinv_l).
+Variable AFth : almost_field_theory.
+Let ARth := AFth.(AF_AR).
+Let rI_neq_rO := AFth.(AF_1_neq_0).
+Let rdiv_def := AFth.(AFdiv_def).
+Let rinv_l := AFth.(AFinv_l).
 
- (* Coefficients *)
- Variable C: Type.
- Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
- Variable ceqb : C->C->bool.
- Variable phi : C -> R.
+Add Morphism radd : radd_ext. Proof. exact (Radd_ext Reqe). Qed.
+Add Morphism rmul : rmul_ext. Proof. exact (Rmul_ext Reqe). Qed.
+Add Morphism ropp : ropp_ext. Proof. exact (Ropp_ext Reqe). Qed.
+Add Morphism rsub : rsub_ext. Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
+Add Morphism rinv : rinv_ext. Proof. exact SRinv_ext. Qed.
 
- Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
+Let eq_trans := Setoid.Seq_trans _ _ Rsth.
+Let eq_sym := Setoid.Seq_sym _ _ Rsth.
+Let eq_refl := Setoid.Seq_refl _ _ Rsth.
+
+Let radd_0_l := ARadd_0_l ARth.
+Let radd_comm := ARadd_comm ARth.
+Let radd_assoc := ARadd_assoc ARth.
+Let rmul_1_l := ARmul_1_l ARth.
+Let rmul_0_l := ARmul_0_l ARth.
+Let rmul_comm := ARmul_comm ARth.
+Let rmul_assoc := ARmul_assoc ARth.
+Let rdistr_l := ARdistr_l ARth.
+Let ropp_mul_l := ARopp_mul_l ARth.
+Let ropp_add := ARopp_add ARth.
+Let rsub_def := ARsub_def ARth.
+
+Let radd_0_r := ARadd_0_r Rsth ARth.
+Let rmul_0_r := ARmul_0_r Rsth ARth.
+Let rmul_1_r := ARmul_1_r Rsth ARth.
+Let ropp_0 := ARopp_zero Rsth Reqe ARth.
+Let rdistr_r := ARdistr_r Rsth Reqe ARth.
+
+(* Coefficients : C *)
+
+Variable C: Type.
+Bind Scope C_scope with C.
+Delimit Scope C_scope with coef.
+
+Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
+Variable ceqb : C->C->bool.
+Variable phi : C -> R.
+
+Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
                                cO cI cadd cmul csub copp ceqb phi.
 
-Lemma ceqb_rect : forall c1 c2 (A:Type) (x y:A) (P:A->Type),
-  (phi c1 == phi c2 -> P x) -> P y -> P (if ceqb c1 c2 then x else y).
+Notation "0" := cO : C_scope.
+Notation "1" := cI : C_scope.
+Infix "+" := cadd : C_scope.
+Infix "-" := csub : C_scope.
+Infix "*" := cmul : C_scope.
+Notation "- x" := (copp x) : C_scope.
+Infix "?=" := ceqb : C_scope.
+Notation "[ x ]" := (phi x) (at level 0).
+
+Let phi_0 := CRmorph.(morph0).
+Let phi_1 := CRmorph.(morph1).
+
+Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c ?= c')%coef.
 Proof.
-intros.
-generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
-case (ceqb c1 c2); auto.
+generalize (CRmorph.(morph_eq) c c').
+destruct (c ?= c')%coef; auto.
 Qed.
 
+(* Power coefficients : Cpow *)
 
- (* C notations *)
- Notation "x +! y" := (cadd x y) (at level 50).
- Notation "x *! y " := (cmul x y) (at level 40).
- Notation "x -! y " := (csub x y) (at level 50).
- Notation "-! x" := (copp x) (at level 35).
- Notation " x ?=! y" := (ceqb x y) (at level 70, no associativity).
- Notation "[ x ]" := (phi x) (at level 0).
+Variable Cpow : Type.
+Variable Cp_phi : N -> Cpow.
+Variable rpow : R -> Cpow -> R.
+Variable pow_th : power_theory rI rmul req Cp_phi rpow.
+(* sign function *)
+Variable get_sign : C -> option C.
+Variable get_sign_spec : sign_theory copp ceqb get_sign.
 
+Variable cdiv:C -> C -> C*C.
+Variable cdiv_th : div_theory req cadd cmul phi cdiv.
 
- (* Useful tactics *)
-  Add Morphism radd : radd_ext.  exact (Radd_ext Reqe). Qed.
-  Add Morphism rmul : rmul_ext.  exact (Rmul_ext Reqe). Qed.
-  Add Morphism ropp : ropp_ext.  exact (Ropp_ext Reqe). Qed.
-  Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
-  Add Morphism rinv : rinv_ext. exact SRinv_ext. Qed.
+Let rpow_pow := pow_th.(rpow_pow_N).
 
-Let eq_trans := Setoid.Seq_trans _ _ Rsth.
-Let eq_sym := Setoid.Seq_sym _ _ Rsth.
-Let eq_refl := Setoid.Seq_refl _ _ Rsth.
-Let mor1h := CRmorph.(morph1).
-
-Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO .
-
-Let lem1 := Rmul_ext Reqe.
-Let lem2 := Rmul_ext Reqe.
-Let lem3 := (Radd_ext Reqe).
-Let lem4 := ARsub_ext Rsth Reqe ARth.
-Let lem5 := Ropp_ext Reqe.
-Let lem6 := ARadd_0_l  ARth.
-Let lem7 := ARadd_comm  ARth.
-Let lem8 := (ARadd_assoc ARth).
-Let lem9 := ARmul_1_l  ARth.
-Let lem10 := (ARmul_0_l  ARth).
-Let lem11 := ARmul_comm  ARth.
-Let lem12 := ARmul_assoc ARth.
-Let lem13 := (ARdistr_l  ARth).
-Let lem14 := ARopp_mul_l ARth.
-Let lem15 := (ARopp_add  ARth).
-Let lem16 := ARsub_def  ARth.
-
-Hint Resolve lem1 lem2 lem3 lem4 lem5 lem6 lem7 lem8 lem9 lem10
-     lem11 lem12 lem13 lem14 lem15 lem16 SRinv_ext.
-
- (* Power coefficients *)
- Variable Cpow : Type.
- Variable Cp_phi : N -> Cpow.
- Variable rpow : R -> Cpow -> R.
- Variable pow_th : power_theory rI rmul req Cp_phi rpow.
- (* sign function *)
- Variable get_sign : C -> option C.
- Variable get_sign_spec : sign_theory copp ceqb get_sign.
-
- Variable cdiv:C -> C -> C*C.
- Variable cdiv_th : div_theory req cadd cmul phi cdiv.
+(* Polynomial expressions : (PExpr C) *)
+
+Bind Scope PE_scope with PExpr.
+Delimit Scope PE_scope with poly.
 
 Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow).
+Notation "P @ l" := (NPEeval l P) (at level 10, no associativity).
+
+Infix "+" := PEadd : PE_scope.
+Infix "-" := PEsub : PE_scope.
+Infix "*" := PEmul : PE_scope.
+Notation "- e" := (PEopp e) : PE_scope.
+Infix "^" := PEpow : PE_scope.
+
+Definition NPEequiv e e' := forall l, e@l == e'@l.
+Infix "===" := NPEequiv (at level 70, no associativity) : PE_scope.
+
+Instance NPEequiv_eq : Equivalence NPEequiv.
+Proof.
+ split; red; unfold NPEequiv; intros; [reflexivity|symmetry|etransitivity];
+  eauto.
+Qed.
+
+Instance NPEeval_ext : Proper (eq ==> NPEequiv ==> req) NPEeval.
+Proof.
+ intros l l' <- e e' He. now rewrite (He l).
+Qed.
+
 Notation Nnorm:= (norm_subst cO cI cadd cmul csub copp ceqb cdiv).
 
 Notation NPphi_dev := (Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign).
@@ -129,17 +166,16 @@ Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi
 (* add abstract semi-ring to help with some proofs *)
 Add Ring Rring : (ARth_SRth ARth).
 
-Local Hint Extern 2 (_ == _) => f_equiv.
-
 (* additional ring properties *)
 
-Lemma rsub_0_l : forall r, 0 - r == - r.
-intros; rewrite (ARsub_def ARth);ring.
+Lemma rsub_0_l r : 0 - r == - r.
+Proof.
+rewrite rsub_def; ring.
 Qed.
 
-Lemma rsub_0_r : forall r, r - 0 == r.
-intros; rewrite (ARsub_def ARth).
-rewrite (ARopp_zero Rsth Reqe ARth);  ring.
+Lemma rsub_0_r r : r - 0 == r.
+Proof.
+rewrite rsub_def, ropp_0; ring.
 Qed.
 
 (***************************************************************************
@@ -148,452 +184,527 @@ Qed.
 
   ***************************************************************************)
 
-Theorem rdiv_simpl: forall p q, ~ q == 0 ->  q * (p / q) == p.
+Theorem rdiv_simpl p q : ~ q == 0 ->  q * (p / q) == p.
 Proof.
-intros p q H.
+intros.
 rewrite rdiv_def.
-transitivity (/ q * q * p); [  ring | idtac ].
-rewrite rinv_l; auto.
+transitivity (/ q * q * p); [ ring | ].
+now rewrite rinv_l.
 Qed.
-Hint Resolve rdiv_simpl .
 
-Instance SRdiv_ext: Proper (req ==> req ==> req) rdiv.
+Instance rdiv_ext: Proper (req ==> req ==> req) rdiv.
 Proof.
-intros p1 p2 Ep q1 q2 Eq.
-transitivity (p1 * / q1); auto.
-transitivity (p2 * / q2); auto.
+intros p1 p2 Ep q1 q2 Eq. now rewrite !rdiv_def, Ep, Eq.
 Qed.
-Hint Resolve SRdiv_ext.
 
-Lemma rmul_reg_l : forall p q1 q2,
+Lemma rmul_reg_l p q1 q2 :
   ~ p == 0 -> p * q1 == p * q2 -> q1 == q2.
 Proof.
-intros p q1 q2 H EQ.
-rewrite <- (@rdiv_simpl q1 p) by trivial.
-rewrite <- (@rdiv_simpl q2 p) by trivial.
-rewrite !rdiv_def, !(ARmul_assoc ARth).
-now rewrite EQ.
+intros H EQ.
+assert (H' : p * (q1 / p) == p * (q2 / p)).
+{ now rewrite !rdiv_def, !rmul_assoc, EQ. }
+now rewrite !rdiv_simpl in H'.
 Qed.
 
-Theorem field_is_integral_domain : forall r1 r2,
+Theorem field_is_integral_domain r1 r2 :
   ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0.
 Proof.
-intros r1 r2 H1 H2. contradict H2.
-transitivity (1 * r2); auto.
-transitivity (/ r1 * r1 * r2); auto.
-rewrite <- (ARmul_assoc ARth).
-rewrite H2.
-apply ARmul_0_r with (1 := Rsth) (2 := ARth).
+intros H1 H2. contradict H2.
+transitivity (/r1 * r1 * r2).
+- now rewrite rinv_l.
+- now rewrite <- rmul_assoc, H2.
 Qed.
 
-Theorem ropp_neq_0 : forall r,
+Theorem ropp_neq_0 r :
   ~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0.
+Proof.
 intros.
 setoid_replace (- r) with (- (1) * r).
- apply field_is_integral_domain; trivial.
- rewrite <- (ARopp_mul_l ARth).
-   rewrite (ARmul_1_l ARth).
-   reflexivity.
+- apply field_is_integral_domain; trivial.
+- now rewrite <- ropp_mul_l, rmul_1_l.
 Qed.
 
-Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1.
-intros.
-rewrite (AFdiv_def AFth).
-rewrite (ARmul_comm ARth).
-apply (AFinv_l AFth).
-trivial.
+Theorem rdiv_r_r r : ~ r == 0 -> r / r == 1.
+Proof.
+intros. rewrite rdiv_def, rmul_comm. now apply rinv_l.
 Qed.
 
-Theorem rdiv1: forall r,  r == r / 1.
-intros r; transitivity (1 * (r / 1)); auto.
+Theorem rdiv1 r : r == r / 1.
+Proof.
+transitivity (1 * (r / 1)).
+- symmetry; apply rdiv_simpl. apply rI_neq_rO.
+- apply rmul_1_l.
 Qed.
 
-Theorem rdiv2:
- forall r1 r2 r3 r4,
- ~ r2 == 0 ->
- ~ r4 == 0 ->
- r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4).
+Theorem rdiv2 a b c d :
+ ~ b == 0 ->
+ ~ d == 0 ->
+ a / b + c / d == (a * d + c * b) / (b * d).
 Proof.
-intros r1 r2 r3 r4 H H0.
-assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
-apply rmul_reg_l with (r2 * r4); trivial.
+intros H H0.
+assert (~ b * d == 0) by now apply field_is_integral_domain.
+apply rmul_reg_l with (b * d); trivial.
 rewrite rdiv_simpl; trivial.
-rewrite (ARdistr_r Rsth Reqe ARth).
-apply (Radd_ext Reqe).
-- transitivity (r2 * (r1 / r2) * r4); [  ring | auto ].
-- transitivity (r2 * (r4 * (r3 / r4))); auto.
-  transitivity (r2 * r3); auto.
+rewrite rdistr_r.
+apply radd_ext.
+- now rewrite <- rmul_assoc, (rmul_comm d), rmul_assoc, rdiv_simpl.
+- now rewrite (rmul_comm c), <- rmul_assoc, rdiv_simpl.
 Qed.
 
 
-Theorem rdiv2b:
- forall r1 r2 r3 r4 r5,
- ~ (r2*r5) == 0 ->
- ~ (r4*r5) == 0 ->
- r1 / (r2*r5) + r3 / (r4*r5) == (r1 * r4 + r3 * r2) / (r2 * (r4 * r5)).
+Theorem rdiv2b a b c d e :
+ ~ (b*e) == 0 ->
+ ~ (d*e) == 0 ->
+ a / (b*e) + c / (d*e) == (a * d + c * b) / (b * (d * e)).
 Proof.
-intros r1 r2 r3 r4 r5 H H0.
-assert (HH1: ~ r2 == 0) by (intros HH; case H; rewrite HH; ring).
-assert (HH2: ~ r5 == 0) by (intros HH; case H; rewrite HH; ring).
-assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring).
-assert (HH4: ~ r2 * (r4 * r5) == 0)
+intros H H0.
+assert (~ b == 0) by (contradict H; rewrite H; ring).
+assert (~ e == 0) by (contradict H; rewrite H; ring).
+assert (~ d == 0) by (contradict H0; rewrite H0; ring).
+assert (~ b * (d * e) == 0)
    by (repeat apply field_is_integral_domain; trivial).
-apply rmul_reg_l with (r2 * (r4 * r5)); trivial.
+apply rmul_reg_l with (b * (d * e)); trivial.
 rewrite rdiv_simpl; trivial.
-rewrite (ARdistr_r Rsth Reqe ARth).
-apply (Radd_ext Reqe).
- transitivity ((r2 * r5) * (r1 / (r2 * r5)) * r4); [  ring | auto ].
- transitivity ((r4 * r5) * (r3 / (r4 * r5)) * r2); [  ring | auto ].
-Qed.
-
-Theorem rdiv5: forall r1 r2,  - (r1 / r2) == - r1 / r2.
-Proof.
-intros r1 r2.
-transitivity (- (r1 * / r2)); auto.
-transitivity (- r1 * / r2); auto.
-Qed.
-Hint Resolve rdiv5 .
-
-Theorem rdiv3 r1 r2 r3 r4 :
- ~ r2 == 0 ->
- ~ r4 == 0 ->
- r1 / r2 - r3 / r4 == (r1 * r4 -  r3 * r2) / (r2 * r4).
-Proof.
-intros H2 H4.
-assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
-transitivity (r1 / r2 + - (r3 / r4)); auto.
-transitivity (r1 / r2 + - r3 / r4); auto.
-transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)).
-apply rdiv2; auto.
-f_equiv.
-transitivity (r1 * r4 + - (r3 * r2)); auto.
-Qed.
-
-
-Theorem rdiv3b:
- forall r1 r2 r3 r4 r5,
- ~ (r2 * r5) == 0 ->
- ~ (r4 * r5) == 0 ->
- r1 / (r2*r5) - r3 / (r4*r5) == (r1 * r4 - r3 * r2) / (r2 * (r4 * r5)).
-Proof.
-intros r1 r2 r3 r4 r5 H H0.
-transitivity (r1 / (r2 * r5) + - (r3 / (r4 * r5))); auto.
-transitivity (r1 / (r2 * r5) + - r3 / (r4 * r5)); auto.
-transitivity ((r1 * r4 + - r3 * r2) / (r2 * (r4 * r5))).
-apply rdiv2b; auto; try ring.
-apply (SRdiv_ext); auto.
-transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto.
-Qed.
-
-Theorem rdiv6:
- forall r1 r2,
- ~ r1 == 0 -> ~ r2 == 0 ->  / (r1 / r2) == r2 / r1.
-intros r1 r2 H H0.
-assert (~ r1 / r2 == 0) as Hk.
- intros H1; case H.
-   transitivity (r2 * (r1 / r2)); auto.
-   rewrite H1;  ring.
- apply rmul_reg_l with (r1 / r2); auto.
-   transitivity (/ (r1 / r2) * (r1 / r2)); auto.
-   transitivity 1; auto.
-   repeat rewrite rdiv_def.
-   transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac |  ring ].
-   repeat rewrite rinv_l; auto.
-Qed.
-Hint Resolve rdiv6 .
-
- Theorem rdiv4:
- forall r1 r2 r3 r4,
- ~ r2 == 0 ->
- ~ r4 == 0 ->
- (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4).
-Proof.
-intros r1 r2 r3 r4 H H0.
-assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
-apply rmul_reg_l with (r2 * r4); trivial.
-rewrite rdiv_simpl; trivial.
-transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [  ring | idtac ].
-repeat rewrite rdiv_simpl; trivial.
+rewrite rdistr_r.
+apply radd_ext.
+- transitivity ((b * e) * (a / (b * e)) * d);
+  [ ring | now rewrite rdiv_simpl ].
+- transitivity ((d * e) * (c / (d * e)) * b);
+  [ ring | now rewrite rdiv_simpl ].
 Qed.
 
- Theorem rdiv4b:
- forall r1 r2 r3 r4 r5 r6,
- ~ r2 * r5 == 0 ->
- ~ r4 * r6 == 0 ->
- ((r1 * r6) / (r2 * r5)) * ((r3 * r5) / (r4 * r6)) == (r1 * r3) / (r2 * r4).
+Theorem rdiv5 a b : - (a / b) == - a / b.
 Proof.
-intros r1 r2 r3 r4 r5 r6 H H0.
-rewrite rdiv4; auto.
-transitivity ((r5 * r6) * (r1 * r3) / ((r5 * r6) * (r2 * r4))).
-apply SRdiv_ext; ring.
-assert (HH: ~ r5*r6 == 0).
-  apply field_is_integral_domain.
-    intros H1; case H; rewrite H1; ring.
-    intros H1; case H0; rewrite H1; ring.
-rewrite <- rdiv4 ; auto.
-  rewrite rdiv_r_r; auto.
+now rewrite !rdiv_def, ropp_mul_l.
+Qed.
 
-  apply field_is_integral_domain.
-    intros H1; case H; rewrite H1; ring.
-    intros H1; case H0; rewrite H1; ring.
+Theorem rdiv3b a b c d e :
+ ~ (b * e) == 0 ->
+ ~ (d * e) == 0 ->
+ a / (b*e) - c / (d*e) == (a * d - c * b) / (b * (d * e)).
+Proof.
+intros H H0.
+rewrite !rsub_def, rdiv5, ropp_mul_l.
+now apply rdiv2b.
 Qed.
 
+Theorem rdiv6 a b :
+ ~ a == 0 -> ~ b == 0 ->  / (a / b) == b / a.
+Proof.
+intros H H0.
+assert (Hk : ~ a / b == 0).
+{ contradict H.
+  transitivity (b * (a / b)).
+  - now rewrite rdiv_simpl.
+  - rewrite H. apply rmul_0_r. }
+apply rmul_reg_l with (a / b); trivial.
+rewrite (rmul_comm (a / b)), rinv_l; trivial.
+rewrite !rdiv_def.
+transitivity (/ a * a * (/ b * b)); [ | ring ].
+now rewrite !rinv_l, rmul_1_l.
+Qed.
+
+Theorem rdiv4 a b c d :
+ ~ b == 0 ->
+ ~ d == 0 ->
+ (a / b) * (c / d) == (a * c) / (b * d).
+Proof.
+intros H H0.
+assert (~ b * d == 0) by now apply field_is_integral_domain.
+apply rmul_reg_l with (b * d); trivial.
+rewrite rdiv_simpl; trivial.
+transitivity (b * (a / b) * (d * (c / d))); [ ring | ].
+rewrite !rdiv_simpl; trivial.
+Qed.
 
-Theorem rdiv7:
- forall r1 r2 r3 r4,
- ~ r2 == 0 ->
- ~ r3 == 0 ->
- ~ r4 == 0 ->
- (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3).
+Theorem rdiv4b a b c d e f :
+ ~ b * e == 0 ->
+ ~ d * f == 0 ->
+ ((a * f) / (b * e)) * ((c * e) / (d * f)) == (a * c) / (b * d).
+Proof.
+intros H H0.
+assert (~ b == 0) by (contradict H; rewrite H; ring).
+assert (~ e == 0) by (contradict H; rewrite H; ring).
+assert (~ d == 0) by (contradict H0; rewrite H0; ring).
+assert (~ f == 0) by (contradict H0; rewrite H0; ring).
+assert (~ b*d == 0) by now apply field_is_integral_domain.
+assert (~ e*f == 0) by now apply field_is_integral_domain.
+rewrite rdiv4; trivial.
+transitivity ((e * f) * (a * c) / ((e * f) * (b * d))).
+- apply rdiv_ext; ring.
+- rewrite <- rdiv4, rdiv_r_r; trivial.
+Qed.
+
+Theorem rdiv7 a b c d :
+ ~ b == 0 ->
+ ~ c == 0 ->
+ ~ d == 0 ->
+ (a / b) / (c / d) == (a * d) / (b * c).
 Proof.
 intros.
-rewrite (rdiv_def (r1 / r2)).
+rewrite (rdiv_def (a / b)).
 rewrite rdiv6; trivial.
 apply rdiv4; trivial.
 Qed.
 
-Theorem rdiv7b:
- forall r1 r2 r3 r4 r5 r6,
- ~ r2 * r6 == 0 ->
- ~ r3 * r5 == 0 ->
- ~ r4 * r6 == 0 ->
- ((r1 * r5) / (r2 * r6)) / ((r3 * r5) / (r4 * r6)) == (r1 * r4) / (r2 * r3).
+Theorem rdiv7b a b c d e f :
+ ~ b * f == 0 ->
+ ~ c * e == 0 ->
+ ~ d * f == 0 ->
+ ((a * e) / (b * f)) / ((c * e) / (d * f)) == (a * d) / (b * c).
+Proof.
+intros Hbf Hce Hdf.
+assert (~ c==0) by (contradict Hce; rewrite Hce; ring).
+assert (~ e==0) by (contradict Hce; rewrite Hce; ring).
+assert (~ b==0) by (contradict Hbf; rewrite Hbf; ring).
+assert (~ f==0) by (contradict Hbf; rewrite Hbf; ring).
+assert (~ b*c==0) by now apply field_is_integral_domain.
+assert (~ e*f==0) by now apply field_is_integral_domain.
+rewrite rdiv7; trivial.
+transitivity ((e * f) * (a * d) / ((e * f) * (b * c))).
+- apply rdiv_ext; ring.
+- now rewrite <- rdiv4, rdiv_r_r.
+Qed.
+
+Theorem rinv_nz a : ~ a == 0 -> ~ /a == 0.
+Proof.
+intros H H0. apply rI_neq_rO.
+rewrite <- (rdiv_r_r H), rdiv_def, H0. apply rmul_0_r.
+Qed.
+
+Theorem rdiv8 a b : ~ b == 0 -> a == 0 ->  a / b == 0.
+Proof.
+intros H H0.
+now rewrite rdiv_def, H0, rmul_0_l.
+Qed.
+
+Theorem cross_product_eq a b c d :
+  ~ b == 0 -> ~ d == 0 -> a * d == c * b -> a / b == c / d.
 Proof.
 intros.
-rewrite rdiv7; auto.
-transitivity ((r5 * r6) * (r1 * r4) / ((r5 * r6) * (r2 * r3))).
-apply SRdiv_ext; ring.
-assert (HH: ~ r5*r6 == 0).
-  apply field_is_integral_domain.
-    intros H2; case H0; rewrite H2; ring.
-    intros H2; case H1; rewrite H2; ring.
-rewrite <- rdiv4 ; auto.
-rewrite rdiv_r_r; auto.
-  apply field_is_integral_domain.
-    intros H2; case H; rewrite H2; ring.
-    intros H2; case H0; rewrite H2; ring.
+transitivity (a / b * (d / d)).
+- now rewrite rdiv_r_r, rmul_1_r.
+- now rewrite rdiv4, H1, (rmul_comm b d), <- rdiv4, rdiv_r_r.
 Qed.
 
+(* Results about [pow_pos] and [pow_N] *)
 
-Theorem rdiv8: forall r1 r2, ~ r2 == 0 -> r1 == 0 ->  r1 / r2 == 0.
-intros r1 r2 H H0.
-transitivity (r1 * / r2); auto.
-transitivity (0 * / r2); auto.
+Instance pow_ext : Proper (req ==> eq ==> req) (pow_pos rmul).
+Proof.
+intros x y H p p' <-. induction p as [p IH| p IH|];simpl; trivial; now rewrite !IH, ?H.
 Qed.
 
+Instance pow_N_ext : Proper (req ==> eq ==> req) (pow_N rI rmul).
+Proof.
+intros x y H n n' <-. destruct n; simpl; trivial. now apply pow_ext.
+Qed.
 
-Theorem cross_product_eq : forall r1 r2 r3 r4,
-  ~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4.
-intros.
-transitivity (r1 / r2 * (r4 / r4)).
- rewrite rdiv_r_r; trivial.
-   symmetry .
-   apply (ARmul_1_r Rsth ARth).
- rewrite rdiv4; trivial.
-   rewrite H1.
-   rewrite (ARmul_comm ARth r2 r4).
-   rewrite <- rdiv4; trivial.
-   rewrite rdiv_r_r by trivial.
-  apply (ARmul_1_r Rsth ARth).
+Lemma pow_pos_0 p : pow_pos rmul 0 p == 0.
+Proof.
+induction p;simpl;trivial; now rewrite !IHp.
+Qed.
+
+Lemma pow_pos_1 p : pow_pos rmul 1 p == 1.
+Proof.
+induction p;simpl;trivial; ring [IHp].
+Qed.
+
+Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p].
+Proof.
+induction p;simpl;trivial; now rewrite !CRmorph.(morph_mul), !IHp.
+Qed.
+
+Lemma pow_pos_mul_l x y p :
+ pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p.
+Proof.
+induction p;simpl;trivial; ring [IHp].
+Qed.
+
+Lemma pow_pos_add_r x p1 p2 :
+ pow_pos rmul x (p1+p2) == pow_pos rmul x p1 * pow_pos rmul x p2.
+Proof.
+ exact (Ring_theory.pow_pos_add Rsth rmul_ext rmul_assoc x p1 p2).
+Qed.
+
+Lemma pow_pos_mul_r x p1 p2 :
+  pow_pos rmul x (p1*p2) == pow_pos rmul (pow_pos rmul x p1) p2.
+Proof.
+induction p1;simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r;
+ simpl; trivial; ring [IHp1].
+Qed.
+
+Lemma pow_pos_nz x p : ~x==0 -> ~pow_pos rmul x p == 0.
+Proof.
+ intros Hx. induction p;simpl;trivial;
+  repeat (apply field_is_integral_domain; trivial).
+Qed.
+
+Lemma pow_pos_div a b p : ~ b == 0 ->
+ pow_pos rmul (a / b) p == pow_pos rmul a p / pow_pos rmul b p.
+Proof.
+ intros.
+ induction p; simpl; trivial.
+ - rewrite IHp.
+   assert (nz := pow_pos_nz p H).
+   rewrite !rdiv4; trivial.
+   apply field_is_integral_domain; trivial.
+ - rewrite IHp.
+   assert (nz := pow_pos_nz p H).
+   rewrite !rdiv4; trivial.
+Qed.
+
+(* === is a morphism *)
+
+Instance PEadd_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEadd C).
+Proof. intros ? ? E ? ? E' l. simpl. now rewrite E, E'. Qed.
+Instance PEsub_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEsub C).
+Proof. intros ? ? E ? ? E' l. simpl. now rewrite E, E'. Qed.
+Instance PEmul_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEmul C).
+Proof. intros ? ? E ? ? E' l. simpl. now rewrite E, E'. Qed.
+Instance PEopp_ext : Proper (NPEequiv ==> NPEequiv) (@PEopp C).
+Proof. intros ? ? E l. simpl. now rewrite E. Qed.
+Instance PEpow_ext : Proper (NPEequiv ==> eq ==> NPEequiv) (@PEpow C).
+Proof.
+ intros ? ? E ? ? <- l. simpl. rewrite !rpow_pow. apply pow_N_ext; trivial.
+Qed.
+
+Arguments PEc _ _%coef.
+
+Lemma PE_1_l (e : PExpr C) : (PEc 1 * e === e)%poly.
+Proof.
+ intros l. simpl. rewrite phi_1. apply rmul_1_l.
+Qed.
+
+Lemma PE_1_r (e : PExpr C) : (e * PEc 1 === e)%poly.
+Proof.
+ intros l. simpl. rewrite phi_1. apply rmul_1_r.
 Qed.
 
+Lemma PEpow_0_r (e : PExpr C) : (e ^ 0 === PEc 1)%poly.
+Proof.
+ intros l. simpl. now rewrite !rpow_pow.
+Qed.
+
+Lemma PEpow_1_r (e : PExpr C) : (e ^ 1 === e)%poly.
+Proof.
+ intros l. simpl. now rewrite !rpow_pow.
+Qed.
+
+Lemma PEpow_1_l n : ((PEc 1) ^ n === PEc 1)%poly.
+Proof.
+ intros l. simpl. rewrite rpow_pow. destruct n; simpl.
+ - now rewrite phi_1.
+ - now rewrite phi_1, pow_pos_1.
+Qed.
+
+Lemma PEpow_add_r (e : PExpr C) n n' :
+ (e ^ (n+n') === e ^ n * e ^ n')%poly.
+Proof.
+ intros l. simpl. rewrite !rpow_pow.
+ destruct n; simpl.
+ - rewrite rmul_1_l. trivial.
+ - destruct n'; simpl.
+   + rewrite rmul_1_r. trivial.
+   + apply pow_pos_add_r.
+Qed.
+
+Lemma PEpow_mul_l (e e' : PExpr C) n :
+ ((e * e') ^ n === e ^ n * e' ^ n)%poly.
+Proof.
+ intros l. simpl. rewrite !rpow_pow. destruct n; simpl; trivial.
+ - symmetry; apply rmul_1_l.
+ - apply pow_pos_mul_l.
+Qed.
+
+Lemma PEpow_mul_r (e : PExpr C) n n' :
+ (e ^ (n * n') === (e ^ n) ^ n')%poly.
+Proof.
+ intros l. simpl. rewrite !rpow_pow.
+ destruct n, n'; simpl; trivial.
+ - now rewrite pow_pos_1.
+ - apply pow_pos_mul_r.
+Qed.
+
+Lemma PEpow_nz l e n : ~ e @ l == 0 -> ~ (e^n) @ l == 0.
+Proof.
+ intros. simpl. rewrite rpow_pow. destruct n; simpl.
+ - apply rI_neq_rO.
+ - now apply pow_pos_nz.
+Qed.
+
+
 (***************************************************************************
 
                        Some equality test
 
   ***************************************************************************)
 
+Local Notation "a &&& b" := (if a then b else false)
+ (at level 40, left associativity).
+
 (* equality test *)
-Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
- match e1, e2 with
-   PEc c1, PEc c2 => ceqb c1 c2
-  | PEX _ p1, PEX _ p2 => Pos.eqb p1 p2
-  | PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
-  | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
-  | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
-  | PEopp e3, PEopp e4 => PExpr_eq e3 e4
-  | PEpow e3 n3, PEpow e4 n4 => if N.eqb n3 n4 then PExpr_eq e3 e4 else false
+Fixpoint PExpr_eq (e e' : PExpr C) {struct e} : bool :=
+ match e, e' with
+   PEc c, PEc c' => ceqb c c'
+  | PEX _ p, PEX _ p' => Pos.eqb p p'
+  | e1 + e2, e1' + e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
+  | e1 - e2, e1' - e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
+  | e1 * e2, e1' * e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
+  | - e, - e' => PExpr_eq e e'
+  | e ^ n, e' ^ n' => N.eqb n n' &&& PExpr_eq e e'
   | _, _ => false
- end.
+ end%poly.
+
+Lemma if_true (a b : bool) : a &&& b = true -> a = true /\ b = true.
+Proof.
+ destruct a, b; split; trivial.
+Qed.
+
+Theorem PExpr_eq_semi_ok e e' :
+ PExpr_eq e e' = true ->  (e === e')%poly.
+Proof.
+revert e'; induction e; destruct e'; simpl; try discriminate.
+- intros H l. now apply (morph_eq CRmorph).
+- case Pos.eqb_spec; intros; now subst.
+- intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2.
+- intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2.
+- intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2.
+- intros H. now rewrite IHe.
+- intros H. destruct (if_true _ _ H).
+  apply N.eqb_eq in H0. now rewrite IHe, H0.
+Qed.
+
+Lemma PExpr_eq_spec e e' : BoolSpec (e === e')%poly True (PExpr_eq e e').
+Proof.
+ assert (H := PExpr_eq_semi_ok e e').
+ destruct PExpr_eq; constructor; intros; trivial. now apply H.
+Qed.
+
+(** Smart constructors for polynomial expression,
+    with reduction of constants *)
 
-Add Morphism (pow_pos rmul) with signature req ==> eq ==> req as pow_morph.
-intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH].
-Qed.
-
-Add Morphism (pow_N rI rmul) with signature req ==> eq ==> req as pow_N_morph.
-intros x y H [|p];simpl;auto. apply pow_morph;trivial.
-Qed.
-
-Theorem PExpr_eq_semi_correct:
- forall l e1 e2, PExpr_eq e1 e2 = true ->  NPEeval l e1 == NPEeval l e2.
-intros l e1; elim e1.
-intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)).
-intros c2; apply (morph_eq CRmorph).
-intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)).
-intros p2; case Pos.eqb_spec; intros; now subst.
-intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
-intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
- (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
- (try (intros; discriminate)); auto.
-intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
-intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
- (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
- (try (intros; discriminate)); auto.
-intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
-intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
- (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
- (try (intros; discriminate)); auto.
-intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))).
-intros e4; generalize (rec e4); case (PExpr_eq e3 e4);
- (try (intros; discriminate)); auto.
-intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))).
-intros e4 n4; case N.eqb_spec; try discriminate; intros EQ H; subst.
-repeat rewrite  pow_th.(rpow_pow_N). rewrite (rec _ H);auto.
-Qed.
-
-(* add *)
 Definition NPEadd e1 e2 :=
   match e1, e2 with
-    PEc c1, PEc c2 => PEc (cadd c1 c2)
-  | PEc c, _ => if ceqb c cO then e2 else PEadd e1 e2
-  |  _, PEc c => if ceqb c cO then e1 else PEadd e1 e2
+  | PEc c1, PEc c2 => PEc (c1 + c2)
+  | PEc c, _ => if (c ?= cO)%coef then e2 else e1 + e2
+  |  _, PEc c => if (c ?= cO)%coef then e1 else e1 + e2
     (* Peut t'on factoriser ici ??? *)
-  | _, _ => PEadd e1 e2
-  end.
+  | _, _ => e1 + e2
+  end%poly.
+Infix "++" := NPEadd (at level 60, right associativity).
 
-Theorem NPEadd_correct:
- forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2).
+Theorem NPEadd_ok e1 e2 : (e1 ++ e2 === e1 + e2)%poly.
 Proof.
-intros l e1 e2.
-destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect;
- try (intro eq_c; rewrite eq_c); simpl;try apply eq_refl;
- try (ring [(morph0 CRmorph)]).
- apply (morph_add CRmorph).
+intros l.
+destruct e1, e2; simpl; try reflexivity; try (case ceqb_spec);
+try intro H; try rewrite H; simpl;
+try apply eq_refl; try (ring [phi_0]).
+apply (morph_add CRmorph).
+Qed.
+
+Definition NPEsub e1 e2 :=
+  match e1, e2 with
+  | PEc c1, PEc c2 => PEc (c1 - c2)
+  | PEc c, _ => if (c ?=cO)%coef then - e2 else e1 - e2
+  |  _, PEc c => if (c ?= cO)%coef then e1 else e1 - e2
+     (* Peut-on factoriser ici *)
+  | _, _ => e1 - e2
+  end%poly.
+Infix "--" := NPEsub (at level 50, left associativity).
+
+Theorem NPEsub_ok e1 e2: (e1 -- e2 === e1 - e2)%poly.
+Proof.
+intros l.
+destruct e1, e2; simpl; try reflexivity; try case ceqb_spec;
+ try intro H; try rewrite H; simpl;
+ try rewrite phi_0; try reflexivity;
+ try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r).
+apply (morph_sub CRmorph).
+Qed.
+
+Definition NPEopp e1 :=
+  match e1 with PEc c1 => PEc (- c1) | _ => - e1 end%poly.
+
+Theorem NPEopp_ok e : (NPEopp e === -e)%poly.
+Proof.
+intros l. destruct e; simpl; trivial. apply (morph_opp CRmorph).
 Qed.
 
 Definition NPEpow x n :=
   match n with
   | N0 => PEc cI
   | Npos p =>
-    if Pos.eqb p xH then x else
+    if Pos.eqb p 1 then x else
     match x with
     | PEc c =>
-      if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p)
-    | _ => PEpow x n
+      if (c ?= 1)%coef then PEc cI
+      else if (c ?= 0)%coef then PEc cO
+      else PEc (pow_pos cmul c p)
+    | _ => x ^ n
     end
-  end.
+  end%poly.
+Infix "^^" := NPEpow (at level 35, right associativity).
 
-Theorem NPEpow_correct : forall l e n,
-  NPEeval l (NPEpow e n) == NPEeval l (PEpow e n).
+Theorem NPEpow_ok e n : (e ^^ n === e ^ n)%poly.
 Proof.
- destruct n;simpl.
- rewrite pow_th.(rpow_pow_N);simpl;auto.
- fold (p =? 1)%positive.
- case Pos.eqb_spec; intros H; (rewrite H || clear H).
- now rewrite  pow_th.(rpow_pow_N).
- destruct e;simpl;auto.
- repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl.
- symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)].
- symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)].
- induction p;simpl;auto;repeat rewrite CRmorph.(morph_mul);ring [IHp].
+ intros l. unfold NPEpow; destruct n.
+ - simpl; now rewrite rpow_pow.
+ - case Pos.eqb_spec; [intro; subst | intros _].
+   + simpl. now rewrite rpow_pow.
+   + destruct e;simpl;trivial.
+     repeat case ceqb_spec; intros; rewrite ?rpow_pow, ?H; simpl.
+     * now rewrite phi_1, pow_pos_1.
+     * now rewrite phi_0, pow_pos_0.
+     * now rewrite pow_pos_cst.
 Qed.
 
-(* mul *)
 Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C :=
   match x, y with
-    PEc c1, PEc c2 => PEc (cmul c1 c2)
+    PEc c1, PEc c2 => PEc (c1 * c2)
   | PEc c, _ =>
-      if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y
+      if (c ?= 1)%coef then y else if (c ?= 0)%coef then PEc cO else x * y
   |  _, PEc c =>
-      if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y
-  | PEpow e1 n1, PEpow e2 n2 =>
-      if N.eqb n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y
-  | _, _ => PEmul x y
-  end.
-
-Lemma pow_pos_mul : forall x y p, pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p.
-induction p;simpl;auto;try ring [IHp].
-Qed.
-
-Theorem NPEmul_correct : forall l e1 e2,
-  NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2).
-induction e1;destruct e2; simpl;try reflexivity;
- repeat apply ceqb_rect;
- try (intro eq_c; rewrite eq_c); simpl; try reflexivity;
- try ring [(morph0 CRmorph) (morph1 CRmorph)].
+      if (c ?= 1)%coef then x else if (c ?= 0)%coef then PEc cO else x * y
+  | e1 ^ n1, e2 ^ n2 =>
+      if N.eqb n1 n2 then (NPEmul e1 e2)^^n1 else x * y
+  | _, _ => x * y
+  end%poly.
+Infix "**" := NPEmul (at level 40, left associativity).
+
+Theorem NPEmul_ok e1 e2 : (e1 ** e2 === e1 * e2)%poly.
+Proof.
+intros l.
+revert e2; induction e1;destruct e2; simpl;try reflexivity;
+ repeat (case ceqb_spec; intro H; try rewrite H; clear H);
+ simpl; try reflexivity; try ring [phi_0 phi_1].
  apply (morph_mul CRmorph).
-case N.eqb_spec; intros H; try rewrite <- H; clear H.
-rewrite NPEpow_correct. simpl.
-repeat rewrite pow_th.(rpow_pow_N).
-rewrite IHe1; destruct n;simpl;try ring.
-apply pow_pos_mul.
-simpl;auto.
-Qed.
-
-(* sub *)
-Definition NPEsub e1 e2 :=
-  match e1, e2 with
-    PEc c1, PEc c2 => PEc (csub c1 c2)
-  | PEc c, _ => if ceqb c cO then PEopp e2 else PEsub e1 e2
-  |  _, PEc c => if ceqb c cO then e1 else PEsub e1 e2
-     (* Peut-on factoriser ici *)
-  | _, _ => PEsub e1 e2
-  end.
-
-Theorem NPEsub_correct:
- forall l e1 e2,  NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2).
-intros l e1 e2.
-destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect;
- try (intro eq_c; rewrite eq_c); simpl;
- try rewrite (morph0 CRmorph); try reflexivity;
- try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r).
-apply (morph_sub CRmorph).
-Qed.
-
-(* opp *)
-Definition NPEopp e1 :=
-  match e1 with PEc c1 => PEc (copp c1) | _ => PEopp e1 end.
-
-Theorem NPEopp_correct:
- forall l e1,  NPEeval l (NPEopp e1) == NPEeval l (PEopp e1).
-intros l e1; case e1; simpl; auto.
-intros; apply (morph_opp CRmorph).
+case N.eqb_spec; [intros <- | reflexivity].
+rewrite NPEpow_ok. simpl.
+rewrite !rpow_pow. rewrite IHe1.
+destruct n; simpl; [ ring | apply pow_pos_mul_l ].
 Qed.
 
 (* simplification *)
-Fixpoint PExpr_simp (e : PExpr C) : PExpr C :=
+Fixpoint PEsimp (e : PExpr C) : PExpr C :=
  match e with
-   PEadd e1 e2 => NPEadd (PExpr_simp e1) (PExpr_simp e2)
-  | PEmul e1 e2 => NPEmul (PExpr_simp e1) (PExpr_simp e2)
-  | PEsub e1 e2 => NPEsub (PExpr_simp e1) (PExpr_simp e2)
-  | PEopp e1 => NPEopp (PExpr_simp e1)
-  | PEpow e1 n1 => NPEpow (PExpr_simp e1) n1
+  | e1 + e2 => (PEsimp e1) ++ (PEsimp e2)
+  | e1 * e2 => (PEsimp e1) ** (PEsimp e2)
+  | e1 - e2 => (PEsimp e1) -- (PEsimp e2)
+  | - e1 => NPEopp (PEsimp e1)
+  | e1 ^ n1 => (PEsimp e1) ^^ n1
   | _ => e
- end.
+ end%poly.
 
-Theorem PExpr_simp_correct:
- forall l e,  NPEeval l (PExpr_simp e) == NPEeval l e.
-intros l e; elim e; simpl; auto.
-intros e1 He1 e2 He2.
-transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto.
-apply NPEadd_correct.
-simpl; auto.
-intros e1 He1 e2 He2.
-transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))); auto.
-apply NPEsub_correct.
-simpl; auto.
-intros e1 He1 e2 He2.
-transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto.
-apply NPEmul_correct.
-simpl; auto.
-intros e1 He1.
-transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto.
-apply NPEopp_correct.
-simpl; auto.
-intros e1 He1 n;simpl.
-rewrite NPEpow_correct;simpl.
-repeat rewrite pow_th.(rpow_pow_N).
-rewrite He1;auto.
+Theorem PEsimp_ok e : (PEsimp e === e)%poly.
+Proof.
+induction e; simpl.
+- intro l; trivial.
+- intro l; trivial.
+- rewrite NPEadd_ok. now f_equiv.
+- rewrite NPEsub_ok. now f_equiv.
+- rewrite NPEmul_ok. now f_equiv.
+- rewrite NPEopp_ok. now f_equiv.
+- rewrite NPEpow_ok. now f_equiv.
 Qed.
 
 
@@ -647,44 +758,46 @@ Record linear : Type := mk_linear {
 Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop :=
   match le with
   | nil => True
-  | e1 :: nil => ~ req (NPEeval l e1) rO
-  | e1 :: l1 => ~ req (NPEeval l e1) rO /\ PCond l l1
+  | e1 :: nil => ~ req (e1 @ l) rO
+  | e1 :: l1 => ~ req (e1 @ l) rO /\ PCond l l1
   end.
 
-Theorem PCond_cons_inv_l :
-   forall l a l1, PCond l (a::l1) ->  ~ NPEeval l a == 0.
-intros l a l1 H.
-destruct l1; simpl in H |- *; trivial.
-destruct H; trivial.
+Theorem PCond_cons l a l1 :
+ PCond l (a :: l1) <-> ~ a @ l == 0 /\ PCond l l1.
+Proof.
+destruct l1.
+- simpl. split; [split|destruct 1]; trivial.
+- reflexivity.
 Qed.
 
-Theorem PCond_cons_inv_r : forall l a l1, PCond l (a :: l1) ->  PCond l l1.
-intros l a l1 H.
-destruct l1; simpl in H |- *; trivial.
-destruct H; trivial.
+Theorem PCond_cons_inv_l l a l1 : PCond l (a::l1) ->  ~ a @ l == 0.
+Proof.
+rewrite PCond_cons. now destruct 1.
 Qed.
 
-Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) ->  PCond l l1.
-intros l l1 l2; elim l1; simpl app.
- simpl; auto.
- destruct l0; simpl in *.
-  destruct l2; firstorder.
-  firstorder.
+Theorem PCond_cons_inv_r l a l1 : PCond l (a :: l1) ->  PCond l l1.
+Proof.
+rewrite PCond_cons. now destruct 1.
 Qed.
 
-Theorem PCond_app_inv_r: forall l l1 l2, PCond l (l1 ++ l2) ->  PCond l l2.
-intros l l1 l2; elim l1; simpl app; auto.
-intros a l0 H H0; apply H; apply PCond_cons_inv_r with ( 1 := H0 ).
+Theorem PCond_app l l1 l2 :
+ PCond l (l1 ++ l2) <-> PCond l l1 /\ PCond l l2.
+Proof.
+induction l1.
+- simpl. split; [split|destruct 1]; trivial.
+- simpl app. rewrite !PCond_cons, IHl1. symmetry; apply and_assoc.
 Qed.
 
+
 (* An unsatisfiable condition: issued when a division by zero is detected *)
 Definition absurd_PCond := cons (PEc cO) nil.
 
 Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond.
+Proof.
 unfold absurd_PCond; simpl.
 red; intros.
 apply H.
-apply (morph0 CRmorph).
+apply phi_0.
 Qed.
 
 (***************************************************************************
@@ -693,167 +806,124 @@ Qed.
 
   ***************************************************************************)
 
-Fixpoint isIn (e1:PExpr C)  (p1:positive)
-                      (e2:PExpr C)  (p2:positive) {struct e2}: option (N * PExpr C) :=
+Definition default_isIn e1 p1 e2 p2 :=
+  if PExpr_eq e1 e2 then
+    match Z.pos_sub p1 p2 with
+     | Zpos p => Some (Npos p, PEc cI)
+     | Z0 => Some (N0, PEc cI)
+     | Zneg p => Some (N0, e2 ^^ Npos p)
+    end
+  else None.
+
+Fixpoint isIn e1 p1 e2 p2 {struct e2}: option (N * PExpr C) :=
   match e2 with
-  | PEmul e3 e4 =>
+  | e3 * e4 =>
        match isIn e1 p1 e3 p2 with
-       | Some (N0, e5) => Some (N0, NPEmul e5 (NPEpow e4 (Npos p2)))
+       | Some (N0, e5) => Some (N0, e5 ** (e4 ^^ Npos p2))
        | Some (Npos p, e5) =>
           match isIn e1 p e4 p2 with
-          | Some (n, e6) => Some (n, NPEmul e5 e6)
-          | None => Some (Npos p, NPEmul e5 (NPEpow e4 (Npos p2)))
+          | Some (n, e6) => Some (n, e5 ** e6)
+          | None => Some (Npos p, e5 ** (e4 ^^ Npos p2))
           end
        | None =>
          match isIn e1 p1 e4 p2 with
-         | Some (n, e5) => Some (n,NPEmul (NPEpow e3 (Npos p2)) e5)
+         | Some (n, e5) => Some (n, (e3 ^^ Npos p2) ** e5)
          | None => None
          end
        end
-  | PEpow e3 N0 => None
-  | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pos.mul p3 p2)
-  | _ =>
-     if  PExpr_eq e1 e2 then
-         match Z.pos_sub p1 p2 with
-          | Zpos p => Some (Npos p, PEc cI)
-          | Z0 => Some (N0, PEc cI)
-          | Zneg p => Some (N0, NPEpow e2 (Npos p))
-          end
-     else None
-   end.
+  | e3 ^ N0 => None
+  | e3 ^ Npos p3 => isIn e1 p1 e3 (Pos.mul p3 p2)
+  | _ => default_isIn e1 p1 e2 p2
+   end%poly.
 
  Definition ZtoN z := match z with Zpos p => Npos p | _ => N0 end.
  Definition NtoZ n := match n with Npos p => Zpos p | _ => Z0 end.
 
- Notation pow_pos_add :=
-   (Ring_theory.pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
-
  Lemma Z_pos_sub_gt p q : (p > q)%positive ->
   Z.pos_sub p q = Zpos (p - q).
  Proof. intros; now apply Z.pos_sub_gt, Pos.gt_lt. Qed.
 
  Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption.
 
- Lemma isIn_correct_aux : forall l e1 e2 p1 p2,
-  match
-      (if  PExpr_eq e1 e2 then
-         match Z.sub (Zpos p1) (Zpos p2) with
-          | Zpos p => Some (Npos p, PEc cI)
-          | Z0 => Some (N0, PEc cI)
-          | Zneg p => Some (N0, NPEpow e2 (Npos p))
-          end
-     else None)
-   with
+ Lemma default_isIn_ok e1 e2 p1 p2 :
+  match default_isIn e1 p1 e2 p2 with
    | Some(n, e3) =>
-       NPEeval l (PEpow e2 (Npos p2)) ==
-       NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\
-       (Zpos p1 > NtoZ n)%Z
-   |  _ => True
+       let n' := ZtoN (Zpos p1 - NtoZ n) in
+       (e2 ^ N.pos p2 === e1 ^ n' * e3)%poly
+       /\ (Zpos p1 > NtoZ n)%Z
+   | _ => True
   end.
 Proof.
-  intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2);
-   case (PExpr_eq e1 e2); simpl; auto; intros H.
+  unfold default_isIn.
+  case PExpr_eq_spec; trivial. intros EQ.
   rewrite Z.pos_sub_spec.
-  case Pos.compare_spec;intros;simpl.
-  - repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:reflexivity.
-    subst. rewrite H by trivial. ring [ (morph1 CRmorph)].
-  - fold (p2 - p1 =? 1)%positive.
-    fold (NPEpow e2 (Npos (p2 - p1))).
-    rewrite NPEpow_correct;simpl.
-    repeat rewrite pow_th.(rpow_pow_N);simpl.
-    rewrite H;trivial. split. 2:reflexivity.
-    rewrite <- pow_pos_add. now rewrite Pos.add_comm, Pos.sub_add.
-  - repeat rewrite pow_th.(rpow_pow_N);simpl.
-    rewrite H;trivial.
-    rewrite Z.pos_sub_gt by now apply Pos.sub_decr.
-    replace (p1 - (p1 - p2))%positive with p2;
-    [| rewrite Pos.sub_sub_distr, Pos.add_comm;
-       auto using Pos.add_sub, Pos.sub_decr ].
-    split.
-    simpl. ring [ (morph1 CRmorph)].
-    now apply Z.lt_gt, Pos.sub_decr.
-Qed.
-
-Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2).
-induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_add;simpl.
-ring [(IHp1 p2)]. ring [(IHp1 p2)]. auto.
-Qed.
-
-
-Theorem isIn_correct: forall l e1 p1 e2 p2,
+  case Pos.compare_spec;intros H; split; try reflexivity.
+  - simpl. now rewrite PE_1_r, H, EQ.
+  - rewrite NPEpow_ok, EQ, <- PEpow_add_r. f_equiv.
+    simpl. f_equiv. now rewrite Pos.add_comm, Pos.sub_add.
+  - simpl. rewrite PE_1_r, EQ. f_equiv.
+    rewrite Z.pos_sub_gt by now apply Pos.sub_decr. simpl. f_equiv.
+    rewrite Pos.sub_sub_distr, Pos.add_comm; trivial.
+    rewrite Pos.add_sub; trivial.
+    apply Pos.sub_decr; trivial.
+  - simpl. now apply Z.lt_gt, Pos.sub_decr.
+Qed.
+
+Ltac npe_simpl := rewrite ?NPEmul_ok, ?NPEpow_ok, ?PEpow_mul_l.
+Ltac npe_ring := intro l; simpl; ring.
+
+Theorem isIn_ok e1 p1 e2 p2 :
   match isIn e1 p1 e2 p2 with
    | Some(n, e3) =>
-       NPEeval l (PEpow e2 (Npos p2)) ==
-       NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\
-        (Zpos p1 > NtoZ n)%Z
+       let n' := ZtoN (Zpos p1 - NtoZ n) in
+       (e2 ^ N.pos p2 === e1 ^ n' * e3)%poly
+       /\ (Zpos p1 > NtoZ n)%Z
    |  _ => True
   end.
 Proof.
 Opaque NPEpow.
-intros l e1 p1 e2; generalize p1;clear p1;elim e2; intros;
-  try (refine (isIn_correct_aux l e1 _ p1 p2);fail);simpl isIn.
-generalize (H p1 p2);clear H;destruct (isIn e1 p1 p p2). destruct p3.
-destruct n.
-  simpl. rewrite NPEmul_correct. simpl; rewrite NPEpow_correct;simpl.
-  repeat rewrite pow_th.(rpow_pow_N);simpl.
-  rewrite pow_pos_mul;intros (H,H1);split;[ring[H]|trivial].
-  generalize (H0 p4 p2);clear H0;destruct (isIn e1 p4 p0 p2). destruct p5.
-  destruct n;simpl.
-    rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl.
-    intros (H1,H2) (H3,H4).
-    simpl_pos_sub. simpl in H3.
-    rewrite pow_pos_mul. rewrite H1;rewrite H3.
-    assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
-        (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) ==
-        pow_pos rmul (NPEeval l e1) p4 * pow_pos rmul (NPEeval l e1) (p1 - p4) *
-        NPEeval l p3 *NPEeval l p5) by ring. rewrite H;clear H.
-   rewrite <- pow_pos_add.
-   rewrite Pos.add_comm, Pos.sub_add by (now apply Z.gt_lt in H4).
-   split. symmetry;apply ARth.(ARmul_assoc). reflexivity.
-   repeat rewrite pow_th.(rpow_pow_N);simpl.
-   intros (H1,H2) (H3,H4).
-   simpl_pos_sub. simpl in H1, H3.
-   assert (Zpos p1 > Zpos p6)%Z.
-     apply Zgt_trans with (Zpos p4). exact H4. exact H2.
-  simpl_pos_sub.
-  split. 2:exact H.
-  rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3.
-  assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
-                (pow_pos rmul (NPEeval l e1) (p4 - p6) * NPEeval l p5) ==
-             pow_pos rmul (NPEeval l e1) (p1 - p4) * pow_pos rmul (NPEeval l e1) (p4 - p6) *
-                NPEeval l p3 * NPEeval l p5) by ring. rewrite H0;clear H0.
-  rewrite <- pow_pos_add.
-  replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive.
- rewrite NPEmul_correct. simpl;ring.
-  assert
-     (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
- change  ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
- rewrite <- Z.add_assoc. rewrite (Z.add_assoc  (- Zpos p4)).
- simpl. rewrite Z.pos_sub_diag. simpl. reflexivity.
- unfold Z.sub, Z.opp in H0. simpl in H0.
-  simpl_pos_sub. inversion H0; trivial.
- simpl. repeat rewrite pow_th.(rpow_pow_N).
- intros H1 (H2,H3). simpl_pos_sub.
- rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
- simpl in H2. rewrite pow_th.(rpow_pow_N);simpl.
- rewrite pow_pos_mul. split. ring [H2]. exact H3.
- generalize (H0 p1 p2);clear H0;destruct (isIn e1 p1 p0 p2). destruct p3.
- destruct n;simpl. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
- repeat rewrite pow_th.(rpow_pow_N);simpl.
- intros (H1,H2);split;trivial. rewrite pow_pos_mul;ring [H1].
- rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
- repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul.
- intros (H1, H2);rewrite H1;split.
-   simpl_pos_sub. simpl in H1;ring [H1]. trivial.
- trivial.
- destruct n. trivial.
- generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3.
- destruct n;simpl. repeat rewrite pow_th.(rpow_pow_N). simpl.
- intros (H1,H2);split. rewrite pow_pos_pow_pos. trivial. trivial.
- repeat rewrite pow_th.(rpow_pow_N). simpl.
- intros (H1,H2);split;trivial.
- rewrite pow_pos_pow_pos;trivial.
- trivial.
+revert p1 p2.
+induction e2; intros p1 p2;
+ try refine (default_isIn_ok e1 _ p1 p2); simpl isIn.
+- specialize (IHe2_1 p1 p2).
+  destruct isIn as [([|p],e)|].
+  + split; [|reflexivity].
+    clear IHe2_2.
+    destruct IHe2_1 as (IH,_).
+    npe_simpl. rewrite IH. npe_ring.
+  + specialize (IHe2_2 p p2).
+    destruct isIn as [([|p'],e')|].
+    * destruct IHe2_1 as (IH1,GT1).
+      destruct IHe2_2 as (IH2,GT2).
+      split; [|simpl; apply Zgt_trans with (Z.pos p); trivial].
+      npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl.
+      replace (N.pos p1) with (N.pos p + N.pos (p1 - p))%N.
+      rewrite PEpow_add_r; npe_ring.
+      { simpl. f_equal. rewrite Pos.add_comm, Pos.sub_add. trivial.
+        now apply Pos.gt_lt. }
+    * destruct IHe2_1 as (IH1,GT1).
+      destruct IHe2_2 as (IH2,GT2).
+      assert (Z.pos p1 > Z.pos p')%Z by (now apply Zgt_trans with (Zpos p)).
+      split; [|simpl; trivial].
+      npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl.
+      replace (N.pos (p1 - p')) with (N.pos (p1 - p) + N.pos (p - p'))%N.
+      rewrite PEpow_add_r; npe_ring.
+      { simpl. f_equal. rewrite Pos.add_sub_assoc, Pos.sub_add; trivial.
+        now apply Pos.gt_lt.
+        now apply Pos.gt_lt. }
+    * destruct IHe2_1 as (IH,GT). split; trivial.
+      npe_simpl. rewrite IH. npe_ring.
+  + specialize (IHe2_2 p1 p2).
+    destruct isIn as [(n,e)|]; trivial.
+    destruct IHe2_2 as (IH,GT). split; trivial.
+    set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d.
+    npe_simpl. rewrite IH. npe_ring.
+- destruct n; trivial.
+  specialize (IHe2 p1 (p * p2)%positive).
+  destruct isIn as [(n,e)|]; trivial.
+  destruct IHe2 as (IH,GT). split; trivial.
+  set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d.
+  now rewrite <- PEpow_mul_r.
 Qed.
 
 Record rsplit : Type := mk_rsplit {
@@ -866,90 +936,90 @@ Notation left := rsplit_left.
 Notation right := rsplit_right.
 Notation common := rsplit_common.
 
-Fixpoint split_aux (e1: PExpr C) (p:positive) (e2:PExpr C) {struct e1}: rsplit :=
+Fixpoint split_aux e1 p e2 {struct e1}: rsplit :=
   match e1 with
-  | PEmul e3 e4 =>
+  | e3 * e4 =>
       let r1 := split_aux e3 p e2 in
       let r2 := split_aux e4 p (right r1) in
-          mk_rsplit (NPEmul (left r1) (left r2))
-                    (NPEmul (common r1) (common r2))
+          mk_rsplit (left r1 ** left r2)
+                    (common r1 ** common r2)
                     (right r2)
-  | PEpow e3 N0 => mk_rsplit (PEc cI) (PEc cI) e2
-  | PEpow e3 (Npos p3) => split_aux e3 (Pos.mul p3 p) e2
+  | e3 ^ N0 => mk_rsplit (PEc cI) (PEc cI) e2
+  | e3 ^ Npos p3 => split_aux e3 (Pos.mul p3 p) e2
   | _ =>
        match isIn e1 p e2 xH with
-       | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3
-       | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3
-       | None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2
+       | Some (N0,e3) => mk_rsplit (PEc cI) (e1 ^^ Npos p) e3
+       | Some (Npos q, e3) => mk_rsplit (e1 ^^ Npos q) (e1 ^^ Npos (p - q)) e3
+       | None => mk_rsplit (e1 ^^ Npos p) (PEc cI) e2
        end
-  end.
+  end%poly.
 
-Lemma split_aux_correct_1 : forall l e1 p e2,
-  let res :=  match isIn e1 p e2 xH with
-       | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3
-       | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3
-       | None => mk_rsplit (NPEpow e1  (Npos p)) (PEc cI) e2
-       end in
-       NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left res) (common res))
-   /\
-       NPEeval l e2 == NPEeval l (NPEmul (right res) (common res)).
-Proof.
- intros. unfold res;clear res; generalize (isIn_correct l e1 p e2 xH).
- destruct (isIn e1 p e2 1). destruct p0.
+Lemma split_aux_ok1 e1 p e2 :
+  (let res :=  match isIn e1 p e2 xH with
+       | Some (N0,e3) => mk_rsplit (PEc cI) (e1 ^^ Npos p) e3
+       | Some (Npos q, e3) => mk_rsplit (e1 ^^ Npos q) (e1 ^^ Npos (p - q)) e3
+       | None => mk_rsplit (e1 ^^ Npos p) (PEc cI) e2
+       end
+  in
+  e1 ^ Npos p === left res * common res
+  /\ e2 === right res * common res)%poly.
+Proof.
  Opaque NPEpow NPEmul.
-  destruct n;simpl;
-    (repeat rewrite NPEmul_correct;simpl;
-     repeat rewrite NPEpow_correct;simpl;
-     repeat rewrite pow_th.(rpow_pow_N);simpl).
-  intros (H, Hgt);split;try ring [H CRmorph.(morph1)].
-  intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H].
-  apply Z.gt_lt in Hgt.
-  now rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add.
-  simpl;intros. repeat rewrite NPEmul_correct;simpl.
-  rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)].
-Qed.
-
-Theorem split_aux_correct: forall l e1 p e2,
-  NPEeval l (PEpow e1 (Npos p)) ==
-       NPEeval l (NPEmul (left (split_aux e1 p e2)) (common (split_aux e1 p e2)))
-/\
-  NPEeval l  e2 == NPEeval l (NPEmul (right (split_aux e1 p e2))
-                                   (common (split_aux e1 p e2))).
-Proof.
-intros l; induction e1;intros k e2; try refine (split_aux_correct_1 l _ k e2);simpl.
-generalize (IHe1_1 k e2); clear IHe1_1.
-generalize (IHe1_2 k (rsplit_right (split_aux e1_1 k e2))); clear IHe1_2.
-simpl. repeat (rewrite NPEmul_correct;simpl).
-repeat rewrite pow_th.(rpow_pow_N);simpl.
-intros (H1,H2) (H3,H4);split.
-rewrite pow_pos_mul. rewrite H1;rewrite H3. ring.
-rewrite H4;rewrite H2;ring.
-destruct n;simpl.
-split. repeat rewrite pow_th.(rpow_pow_N);simpl.
-rewrite NPEmul_correct. simpl.
- induction k;simpl;try ring [CRmorph.(morph1)]; ring [IHk CRmorph.(morph1)].
- rewrite NPEmul_correct;simpl. ring [CRmorph.(morph1)].
-generalize (IHe1 (p*k)%positive e2);clear IHe1;simpl.
-repeat rewrite NPEmul_correct;simpl.
-repeat rewrite pow_th.(rpow_pow_N);simpl.
-rewrite pow_pos_pow_pos. intros [H1 H2];split;ring [H1 H2].
+ intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH).
+ destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl.
+ - intros (H1,H2); split; npe_simpl.
+   + now rewrite PE_1_l.
+   + rewrite PEpow_1_r in H1. rewrite H1. npe_ring.
+ - intros (H1,H2); split; npe_simpl.
+   + rewrite <- PEpow_add_r. f_equiv. simpl. f_equal.
+     rewrite Pos.add_comm, Pos.sub_add; trivial.
+     now apply Z.gt_lt in H2.
+   + rewrite PEpow_1_r in H1. rewrite H1. simpl_pos_sub. simpl. npe_ring.
+ - intros _; split; npe_simpl; now rewrite PE_1_r.
+Qed.
+
+Theorem split_aux_ok: forall e1 p e2,
+  (e1 ^ Npos p === left (split_aux e1 p e2) * common (split_aux e1 p e2)
+  /\ e2 === right (split_aux e1 p e2) * common (split_aux e1 p e2))%poly.
+Proof.
+induction e1;intros k e2; try refine (split_aux_ok1 _ k e2);simpl.
+destruct (IHe1_1 k e2) as (H1,H2).
+destruct (IHe1_2 k (right (split_aux e1_1 k e2))) as (H3,H4).
+clear IHe1_1 IHe1_2.
+- npe_simpl; split.
+  * rewrite H1, H3. npe_ring.
+  * rewrite H2 at 1. rewrite H4 at 1. npe_ring.
+- destruct n; simpl.
+  + rewrite PEpow_0_r, PEpow_1_l, !PE_1_r. now split.
+  + rewrite <- PEpow_mul_r. simpl. apply IHe1.
 Qed.
 
 Definition split e1 e2 := split_aux e1 xH e2.
 
-Theorem split_correct_l: forall l e1 e2,
-  NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2))
-                                   (common (split e1 e2))).
+Theorem split_ok_l e1 e2 :
+  (e1 === left (split e1 e2) * common (split e1 e2))%poly.
 Proof.
-intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl.
-rewrite pow_th.(rpow_pow_N);simpl;auto.
+destruct (split_aux_ok e1 xH e2) as (H,_). now rewrite <- H, PEpow_1_r.
 Qed.
 
-Theorem split_correct_r: forall l e1 e2,
-  NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2))
-                                   (common (split e1 e2))).
+Theorem split_ok_r e1 e2 :
+  (e2 === right (split e1 e2) * common (split e1 e2))%poly.
 Proof.
-intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl;auto.
+destruct (split_aux_ok e1 xH e2) as (_,H). trivial.
+Qed.
+
+Lemma split_nz_l l e1 e2 :
+ ~ e1 @ l == 0 -> ~ left (split e1 e2) @ l == 0.
+Proof.
+ intros H. contradict H. rewrite (split_ok_l e1 e2); simpl.
+ now rewrite H, rmul_0_l.
+Qed.
+
+Lemma split_nz_r l e1 e2 :
+ ~ e2 @ l == 0 -> ~ right (split e1 e2) @ l == 0.
+Proof.
+ intros H. contradict H. rewrite (split_ok_r e1 e2); simpl.
+ now rewrite H, rmul_0_l.
 Qed.
 
 Fixpoint Fnorm (e : FExpr) : linear :=
@@ -961,26 +1031,25 @@ Fixpoint Fnorm (e : FExpr) : linear :=
       let y := Fnorm e2 in
       let s := split (denum x) (denum y) in
       mk_linear
-        (NPEadd (NPEmul (num x) (right s)) (NPEmul (num y) (left s)))
-        (NPEmul (left s) (NPEmul (right s) (common s)))
-        (condition x ++ condition y)
-
+        ((num x ** right s) ++ (num y ** left s))
+        (left s ** (right s ** common s))
+        (condition x ++ condition y)%list
   | FEsub e1 e2 =>
       let x := Fnorm e1 in
       let y := Fnorm e2 in
       let s := split (denum x) (denum y) in
       mk_linear
-        (NPEsub (NPEmul (num x) (right s)) (NPEmul (num y) (left s)))
-        (NPEmul (left s) (NPEmul (right s) (common s)))
-        (condition x ++ condition y)
+        ((num x ** right s) -- (num y ** left s))
+        (left s ** (right s ** common s))
+        (condition x ++ condition y)%list
   | FEmul e1 e2 =>
       let x := Fnorm e1 in
       let y := Fnorm e2 in
       let s1 := split (num x) (denum y) in
       let s2 := split (num y) (denum x) in
-      mk_linear (NPEmul (left s1) (left s2))
-        (NPEmul (right s2) (right s1))
-        (condition x ++ condition y)
+      mk_linear (left s1 ** left s2)
+        (right s2 ** right s1)
+        (condition x ++ condition y)%list
   | FEopp e1 =>
       let x := Fnorm e1 in
       mk_linear (NPEopp (num x)) (denum x) (condition x)
@@ -992,15 +1061,14 @@ Fixpoint Fnorm (e : FExpr) : linear :=
       let y := Fnorm e2 in
       let s1 := split (num x) (num y) in
       let s2 := split (denum x) (denum y) in
-      mk_linear (NPEmul (left s1) (right s2))
-        (NPEmul (left s2) (right s1))
-        (num y :: condition x ++ condition y)
+      mk_linear (left s1 ** right s2)
+        (left s2 ** right s1)
+        (num y :: condition x ++ condition y)%list
   | FEpow e1 n =>
       let x := Fnorm e1 in
-      mk_linear (NPEpow (num x) n) (NPEpow (denum x) n) (condition x)
+      mk_linear ((num x)^^n) ((denum x)^^n) (condition x)
   end.
 
-
 (* Example *)
 (*
 Eval compute
@@ -1010,93 +1078,29 @@ Eval compute
           (FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))).
 *)
 
- Lemma pow_pos_not_0 : forall x, ~x==0 -> forall p, ~pow_pos rmul x p == 0.
+Theorem Pcond_Fnorm l e :
+ PCond l (condition (Fnorm e)) ->  ~ (denum (Fnorm e))@l == 0.
 Proof.
- induction p;simpl.
-  intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H).
-  apply IHp.
-  rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
-  reflexivity.
-  rewrite H1. ring. rewrite Hp;ring.
-  intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
-  reflexivity. rewrite Hp;ring. trivial.
-Qed.
-
-Theorem Pcond_Fnorm:
- forall l e,
- PCond l (condition (Fnorm e)) ->  ~ NPEeval l (denum (Fnorm e)) == 0.
-intros l e; elim e.
- simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
- simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-   intros HH; case Hrec1; auto.
-     apply PCond_app_inv_l with (1 := Hcond).
-   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
-   rewrite NPEmul_correct; simpl; rewrite HH; ring.
-   intros HH; case Hrec2; auto.
-     apply PCond_app_inv_r with (1 := Hcond).
-   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-   intros HH; case Hrec1; auto.
-     apply PCond_app_inv_l with (1 := Hcond).
-   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
-   rewrite NPEmul_correct; simpl; rewrite HH; ring.
-   intros HH; case Hrec2; auto.
-     apply PCond_app_inv_r with (1 := Hcond).
-   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-  intros HH; apply Hrec1.
-    apply PCond_app_inv_l with (1 := Hcond).
-    rewrite (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
-  intros HH; apply Hrec2.
-    apply PCond_app_inv_r with (1 := Hcond).
-    rewrite (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
- intros e1 Hrec1 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   auto.
- intros e1 Hrec1 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   apply PCond_cons_inv_l with (1:=Hcond).
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-    intros HH; apply Hrec1.
-    specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1.
-    apply PCond_app_inv_l with (1 := Hcond1).
-    rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
-    intros HH; apply PCond_cons_inv_l with (1:=Hcond).
-    rewrite (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
- simpl;intros e1 Hrec1 n Hcond.
-  rewrite NPEpow_correct.
-  simpl;rewrite pow_th.(rpow_pow_N).
-  destruct n;simpl;intros.
-  apply AFth.(AF_1_neq_0). apply pow_pos_not_0;auto.
-Qed.
-Hint Resolve Pcond_Fnorm.
+induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app;
+ simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok.
+- simpl; intros. rewrite phi_1; exact rI_neq_rO.
+- simpl; intros. rewrite phi_1; exact rI_neq_rO.
+- rewrite <- split_ok_r. simpl. apply field_is_integral_domain.
+  + apply split_nz_l, IHe1, Hc1.
+  + apply IHe2, Hc2.
+- rewrite <- split_ok_r. simpl. apply field_is_integral_domain.
+  + apply split_nz_l, IHe1, Hc1.
+  + apply IHe2, Hc2.
+- simpl. apply field_is_integral_domain.
+  + apply split_nz_r, IHe1, Hc1.
+  + apply split_nz_r, IHe2, Hc2.
+- now apply IHe.
+- trivial.
+- destruct Hc2 as (Hc2,_). simpl. apply field_is_integral_domain.
+  + apply split_nz_l, IHe1, Hc2.
+  + apply split_nz_r, Hc1.
+- rewrite NPEpow_ok. apply PEpow_nz, IHe, Hc.
+Qed.
 
 
 (***************************************************************************
@@ -1105,154 +1109,101 @@ Hint Resolve Pcond_Fnorm.
 
   ***************************************************************************)
 
-Theorem Fnorm_FEeval_PEeval:
- forall l fe,
+Ltac uneval :=
+ repeat match goal with
+  | |- context [ ?x @ ?l * ?y @ ?l ] => change (x@l * y@l) with ((x*y)@l)
+  | |- context [ ?x @ ?l + ?y @ ?l ] => change (x@l + y@l) with ((x+y)@l)
+ end.
+
+Theorem Fnorm_FEeval_PEeval l fe:
  PCond l (condition (Fnorm fe)) ->
- FEeval l fe == NPEeval l (num (Fnorm fe)) / NPEeval l (denum (Fnorm fe)).
-Proof.
-intros l fe; elim fe; simpl.
-intros c H; rewrite CRmorph.(morph1); apply rdiv1.
-intros p H; rewrite CRmorph.(morph1); apply rdiv1.
-intros e1 He1 e2 He2 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_app_inv_l with ( 1 := HH ).
-assert (HH2: PCond l (condition (Fnorm e2))).
-apply PCond_app_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); rewrite (He2 HH2).
-rewrite NPEadd_correct; simpl.
-repeat rewrite NPEmul_correct; simpl.
-generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
-repeat rewrite NPEmul_correct; simpl.
-intros U1 U2; rewrite U1; rewrite U2.
-apply rdiv2b; auto.
-  rewrite <- U1; auto.
-  rewrite <- U2; auto.
-
-intros e1 He1 e2 He2 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_app_inv_l with ( 1 := HH ).
-assert (HH2: PCond l (condition (Fnorm e2))).
-apply PCond_app_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); rewrite (He2 HH2).
-rewrite NPEsub_correct; simpl.
-repeat rewrite NPEmul_correct; simpl.
-generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
-repeat rewrite NPEmul_correct; simpl.
-intros U1 U2; rewrite U1; rewrite U2.
-apply rdiv3b; auto.
-  rewrite <- U1; auto.
-  rewrite <- U2; auto.
-
-intros e1 He1 e2 He2 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_app_inv_l with ( 1 := HH ).
-assert (HH2: PCond l (condition (Fnorm e2))).
-apply PCond_app_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); rewrite (He2 HH2).
-repeat rewrite NPEmul_correct; simpl.
-generalize (split_correct_l l (num (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_l l (num (Fnorm e2)) (denum (Fnorm e1)))
-   (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
-repeat rewrite NPEmul_correct; simpl.
-intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3;
-  rewrite U4; simpl.
-apply rdiv4b; auto.
-  rewrite <- U4; auto.
-  rewrite <- U2; auto.
-
-intros e1 He1 HH.
-rewrite NPEopp_correct; simpl; rewrite (He1 HH); apply rdiv5; auto.
-
-intros e1 He1 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_cons_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); apply rdiv6; auto.
-apply PCond_cons_inv_l with ( 1 := HH ).
-
-intros e1 He1 e2 He2 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_app_inv_l with (condition (Fnorm e2)).
-apply PCond_cons_inv_r with ( 1 := HH ).
-assert (HH2: PCond l (condition (Fnorm e2))).
-apply PCond_app_inv_r with (condition (Fnorm e1)).
-apply PCond_cons_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); rewrite (He2 HH2).
-repeat rewrite NPEmul_correct;simpl.
-generalize (split_correct_l l (num (Fnorm e1)) (num (Fnorm e2)))
-   (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2)))
-   (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
-repeat rewrite NPEmul_correct; simpl.
-intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3;
-  rewrite U4; simpl.
-apply rdiv7b; auto.
-  rewrite <- U3; auto.
-  rewrite <- U2; auto.
-apply PCond_cons_inv_l with ( 1 := HH ).
-  rewrite <- U4; auto.
-
-intros e1 He1 n Hcond;assert (He1' := He1 Hcond);clear He1.
-repeat rewrite NPEpow_correct;simpl;repeat rewrite pow_th.(rpow_pow_N).
-rewrite He1';clear He1'.
-destruct n;simpl. apply rdiv1.
-generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1)))
-  (Pcond_Fnorm _ _ Hcond).
-intros r r0 Hdiff;induction p;simpl.
-repeat (rewrite <- rdiv4;trivial).
-rewrite IHp. reflexivity.
-apply pow_pos_not_0;trivial.
-apply pow_pos_not_0;trivial.
-intro Hp. apply (pow_pos_not_0 Hdiff  p).
-rewrite  (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p)  0).
- reflexivity. apply pow_pos_not_0;trivial. ring [Hp].
-rewrite <- rdiv4;trivial.
-rewrite IHp;reflexivity.
-apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
-reflexivity.
-Qed.
-
-Theorem Fnorm_crossproduct:
- forall l fe1 fe2,
+ FEeval l fe == (num (Fnorm fe)) @ l / (denum (Fnorm fe)) @ l.
+Proof.
+induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl;
+ intros (Hc1,Hc2) || intros Hc;
+ try (specialize (IHfe1 Hc1);apply Pcond_Fnorm in Hc1);
+ try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2);
+ try set (F1 := Fnorm fe1) in *; try set (F2 := Fnorm fe2) in *.
+
+- rewrite phi_1; apply rdiv1.
+- rewrite phi_1; apply rdiv1.
+- rewrite NPEadd_ok, !NPEmul_ok. simpl.
+  rewrite <- rdiv2b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial.
+  now f_equiv.
+
+- rewrite NPEsub_ok, !NPEmul_ok. simpl.
+  rewrite <- rdiv3b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial.
+  now f_equiv.
+
+- rewrite !NPEmul_ok. simpl.
+  rewrite IHfe1, IHfe2.
+  rewrite (split_ok_l (num F1) (denum F2) l),
+          (split_ok_r (num F1) (denum F2) l),
+          (split_ok_l (num F2) (denum F1) l),
+          (split_ok_r (num F2) (denum F1) l) in *.
+  apply rdiv4b; trivial.
+
+- rewrite NPEopp_ok; simpl; rewrite (IHfe Hc); apply rdiv5.
+
+- rewrite (IHfe Hc2); apply rdiv6; trivial;
+   apply Pcond_Fnorm; trivial.
+
+- destruct Hc2 as (Hc2,Hc3).
+  rewrite !NPEmul_ok. simpl.
+  assert (U1 := split_ok_l (num F1) (num F2) l).
+  assert (U2 := split_ok_r (num F1) (num F2) l).
+  assert (U3 := split_ok_l (denum F1) (denum F2) l).
+  assert (U4 := split_ok_r (denum F1) (denum F2) l).
+  rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4; apply rdiv7b;
+   rewrite <- ?U2, <- ?U3, <- ?U4; try apply Pcond_Fnorm; trivial.
+
+- rewrite !NPEpow_ok. simpl. rewrite !rpow_pow, (IHfe Hc).
+  destruct n; simpl.
+  + apply rdiv1.
+  + apply pow_pos_div. apply Pcond_Fnorm; trivial.
+Qed.
+
+Theorem Fnorm_crossproduct l fe1 fe2 :
  let nfe1 := Fnorm fe1 in
  let nfe2 := Fnorm fe2 in
- NPEeval l (PEmul (num nfe1) (denum nfe2)) ==
- NPEeval l (PEmul (num nfe2) (denum nfe1)) ->
+ (num nfe1 * denum nfe2) @ l == (num nfe2 * denum nfe1) @ l ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
-intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2.
-rewrite Fnorm_FEeval_PEeval by
- apply PCond_app_inv_l with (1 := Hcond).
- rewrite Fnorm_FEeval_PEeval by
-  apply PCond_app_inv_r with (1 := Hcond).
-  apply cross_product_eq; trivial.
-   apply Pcond_Fnorm.
-     apply PCond_app_inv_l with (1 := Hcond).
-   apply Pcond_Fnorm.
-     apply PCond_app_inv_r with (1 := Hcond).
+Proof.
+simpl. rewrite PCond_app. intros Hcrossprod (Hc1,Hc2).
+rewrite !Fnorm_FEeval_PEeval; trivial.
+apply cross_product_eq; trivial;
+ apply Pcond_Fnorm; trivial.
 Qed.
 
 (* Correctness lemmas of reflexive tactics *)
 Notation Ninterp_PElist := (interp_PElist rO radd rmul rsub ropp req phi Cp_phi rpow).
 Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv).
 
-Theorem Fnorm_correct:
+Theorem Fnorm_ok:
  forall n l lpe fe,
   Ninterp_PElist l lpe ->
   Peq ceqb (Nnorm n (Nmk_monpol_list lpe) (num (Fnorm fe))) (Pc cO) = true ->
   PCond l (condition (Fnorm fe)) ->  FEeval l fe == 0.
-intros n l lpe fe Hlpe H H1;
- apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1).
-apply rdiv8; auto.
-transitivity (NPEeval l (PEc cO)); auto.
-rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe);auto.
-change (NPEeval l (PEc cO)) with (Pphi 0 radd rmul phi l (Pc cO)).
-apply (Peq_ok Rsth Reqe CRmorph);auto.
-simpl. apply (morph0 CRmorph); auto.
+Proof.
+intros n l lpe fe Hlpe H H1.
+rewrite (Fnorm_FEeval_PEeval l fe H1).
+apply rdiv8. apply Pcond_Fnorm; trivial.
+transitivity ((PEc cO)@l); trivial.
+rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe); trivial.
+change ((PEc cO) @ l) with (Pphi 0 radd rmul phi l (Pc cO)).
+apply (Peq_ok Rsth Reqe CRmorph); trivial.
 Qed.
 
+Notation ring_rw_correct :=
+ (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec).
+
+Notation ring_rw_pow_correct :=
+ (ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec).
+
+Notation ring_correct :=
+ (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th).
+
 (* simplify a field expression into a fraction *)
 (* TODO: simplify when den is constant... *)
 Definition display_linear l num den :=
@@ -1261,71 +1212,49 @@ Definition display_linear l num den :=
 Definition display_pow_linear l num den :=
   NPphi_pow l num / NPphi_pow l den.
 
-Theorem Field_rw_correct :
- forall n lpe l,
+Theorem Field_rw_correct n lpe l :
    Ninterp_PElist l lpe ->
    forall lmp, Nmk_monpol_list lpe = lmp ->
    forall fe nfe, Fnorm fe = nfe ->
    PCond l (condition nfe) ->
    FEeval l fe == display_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
 Proof.
-  intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
-  apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H).
-  unfold display_linear; apply SRdiv_ext;
-  eapply (ring_rw_correct Rsth Reqe ARth CRmorph);eauto.
+  intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
+  rewrite (Fnorm_FEeval_PEeval _ _ H).
+  unfold display_linear; apply rdiv_ext;
+  eapply ring_rw_correct; eauto.
 Qed.
 
-Theorem Field_rw_pow_correct :
- forall n lpe l,
+Theorem Field_rw_pow_correct n lpe l :
    Ninterp_PElist l lpe ->
    forall lmp, Nmk_monpol_list lpe = lmp ->
    forall fe nfe, Fnorm fe = nfe ->
    PCond l (condition nfe) ->
    FEeval l fe == display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
 Proof.
-  intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
-  apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H).
-  unfold display_pow_linear; apply SRdiv_ext;
-  eapply (ring_rw_pow_correct Rsth Reqe ARth CRmorph);eauto.
+  intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
+  rewrite (Fnorm_FEeval_PEeval _ _ H).
+  unfold display_pow_linear; apply rdiv_ext;
+  eapply ring_rw_pow_correct;eauto.
 Qed.
 
-Theorem Field_correct :
- forall n l lpe fe1 fe2, Ninterp_PElist l lpe ->
+Theorem Field_correct n l lpe fe1 fe2 :
+ Ninterp_PElist l lpe ->
  forall lmp, Nmk_monpol_list lpe = lmp ->
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
- Peq ceqb (Nnorm n lmp (PEmul (num nfe1) (denum nfe2)))
-          (Nnorm n lmp (PEmul (num nfe2) (denum nfe1))) = true ->
+ Peq ceqb (Nnorm n lmp (num nfe1 * denum nfe2))
+          (Nnorm n lmp (num nfe2 * denum nfe1)) = true ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 Proof.
-intros n l lpe fe1 fe2 Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp.
+intros Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp.
 apply Fnorm_crossproduct; trivial.
-eapply (ring_correct Rsth Reqe ARth CRmorph); eauto.
+eapply ring_correct; eauto.
 Qed.
 
 (* simplify a field equation : generate the crossproduct and simplify
    polynomials *)
-Theorem Field_simplify_eq_old_correct :
- forall l fe1 fe2 nfe1 nfe2,
- Fnorm fe1 = nfe1 ->
- Fnorm fe2 = nfe2 ->
- NPphi_dev l (Nnorm O nil (PEmul (num nfe1) (denum nfe2))) ==
- NPphi_dev l (Nnorm O nil (PEmul (num nfe2) (denum nfe1))) ->
- PCond l (condition nfe1 ++ condition nfe2) ->
- FEeval l fe1 == FEeval l fe2.
-Proof.
-intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond;  subst nfe1 nfe2.
-apply Fnorm_crossproduct; trivial.
-match goal with
- [ |- NPEeval l ?x == NPEeval l ?y] =>
-    rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
-       O nil l I Logic.eq_refl x Logic.eq_refl);
-    rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
-       O nil l I Logic.eq_refl y Logic.eq_refl)
- end.
-trivial.
-Qed.
 
 Theorem Field_simplify_eq_correct :
  forall n l lpe fe1 fe2,
@@ -1334,37 +1263,24 @@ Theorem Field_simplify_eq_correct :
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
  forall den, split (denum nfe1) (denum nfe2) = den ->
- NPphi_dev l (Nnorm n lmp (PEmul (num nfe1) (right den))) ==
- NPphi_dev l (Nnorm n lmp (PEmul (num nfe2) (left den))) ->
+ NPphi_dev l (Nnorm n lmp (num nfe1 * right den)) ==
+ NPphi_dev l (Nnorm n lmp (num nfe2 * left den)) ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 Proof.
-intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
-  subst nfe1 nfe2 den lmp.
-apply Fnorm_crossproduct; trivial.
+intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond.
+apply Fnorm_crossproduct; rewrite ?eq1, ?eq2; trivial.
 simpl.
-rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
-rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
-rewrite NPEmul_correct.
-rewrite NPEmul_correct.
+rewrite (split_ok_l (denum nfe1) (denum nfe2) l), eq3.
+rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3.
 simpl.
-repeat rewrite (ARmul_assoc ARth).
-rewrite <-(
-  let x := PEmul (num (Fnorm fe1))
-                     (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
-ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe Logic.eq_refl
-        x Logic.eq_refl) in Hcrossprod.
-rewrite <-(
-  let x := (PEmul (num (Fnorm fe2))
-                     (rsplit_left
-                        (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
-    ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe Logic.eq_refl
-        x Logic.eq_refl) in Hcrossprod.
-simpl in Hcrossprod.
-rewrite Hcrossprod.
-reflexivity.
+rewrite !rmul_assoc.
+apply rmul_ext; trivial.
+rewrite
+ (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
+ (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl).
+rewrite Hlmp.
+apply Hcrossprod.
 Qed.
 
 Theorem Field_simplify_eq_pow_correct :
@@ -1374,37 +1290,55 @@ Theorem Field_simplify_eq_pow_correct :
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
  forall den, split (denum nfe1) (denum nfe2) = den ->
- NPphi_pow l (Nnorm n lmp (PEmul (num nfe1) (right den))) ==
- NPphi_pow l (Nnorm n lmp (PEmul (num nfe2) (left den))) ->
+ NPphi_pow l (Nnorm n lmp (num nfe1 * right den)) ==
+ NPphi_pow l (Nnorm n lmp (num nfe2 * left den)) ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 Proof.
-intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
-  subst nfe1 nfe2 den lmp.
-apply Fnorm_crossproduct; trivial.
+intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond.
+apply Fnorm_crossproduct; rewrite ?eq1, ?eq2; trivial.
 simpl.
-rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
-rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
-rewrite NPEmul_correct.
-rewrite NPEmul_correct.
+rewrite (split_ok_l (denum nfe1) (denum nfe2) l), eq3.
+rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3.
 simpl.
-repeat rewrite (ARmul_assoc ARth).
-rewrite <-(
-  let x := PEmul (num (Fnorm fe1))
-                     (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
-ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe Logic.eq_refl
-        x Logic.eq_refl) in Hcrossprod.
-rewrite <-(
-  let x := (PEmul (num (Fnorm fe2))
-                     (rsplit_left
-                        (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
-    ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe Logic.eq_refl
-        x Logic.eq_refl) in Hcrossprod.
-simpl in Hcrossprod.
-rewrite Hcrossprod.
-reflexivity.
+rewrite !rmul_assoc.
+apply rmul_ext; trivial.
+rewrite
+ (ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
+ (ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl).
+rewrite Hlmp.
+apply Hcrossprod.
+Qed.
+
+Theorem Field_simplify_aux_ok l fe1 fe2 den :
+ FEeval l fe1 == FEeval l fe2 ->
+ split (denum (Fnorm fe1)) (denum (Fnorm fe2)) = den ->
+ PCond l (condition (Fnorm fe1) ++ condition (Fnorm fe2)) ->
+ (num (Fnorm fe1) * right den) @ l == (num (Fnorm fe2) * left den) @ l.
+Proof.
+ rewrite PCond_app; intros Hfe Hden (Hc1,Hc2); simpl.
+ assert (Hc1' := Pcond_Fnorm _ _ Hc1).
+ assert (Hc2' := Pcond_Fnorm _ _ Hc2).
+ set (N1 := num (Fnorm fe1)) in *. set (N2 := num (Fnorm fe2)) in *.
+ set (D1 := denum (Fnorm fe1)) in *. set (D2 := denum (Fnorm fe2)) in *.
+ assert (~ (common den) @ l == 0).
+ { intro H. apply Hc1'.
+   rewrite (split_ok_l D1 D2 l).
+   rewrite Hden. simpl. ring [H]. }
+ apply (@rmul_reg_l ((common den) @ l)); trivial.
+ rewrite !(rmul_comm ((common den) @ l)), <- !rmul_assoc.
+ change
+  (N1@l * (right den * common den) @ l ==
+   N2@l * (left den * common den) @ l).
+ rewrite <- Hden, <- split_ok_l, <- split_ok_r.
+ apply (@rmul_reg_l (/ D2@l)). { apply rinv_nz; trivial. }
+ rewrite (rmul_comm (/ D2 @ l)), <- !rmul_assoc.
+ rewrite <- rdiv_def, rdiv_r_r, rmul_1_r by trivial.
+ apply (@rmul_reg_l (/ (D1@l))). { apply rinv_nz; trivial. }
+ rewrite !(rmul_comm  (/ D1@l)), <- !rmul_assoc.
+ rewrite <- !rdiv_def, rdiv_r_r, rmul_1_r by trivial.
+ rewrite (rmul_comm (/ D2@l)), <- rdiv_def.
+ unfold N1,N2,D1,D2; rewrite <- !Fnorm_FEeval_PEeval; trivial.
 Qed.
 
 Theorem Field_simplify_eq_pow_in_correct :
@@ -1414,47 +1348,17 @@ Theorem Field_simplify_eq_pow_in_correct :
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
  forall den, split (denum nfe1) (denum nfe2) = den ->
- forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 ->
- forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 ->
+ forall np1, Nnorm n lmp (num nfe1 * right den) = np1 ->
+ forall np2, Nnorm n lmp (num nfe2 * left den) = np2 ->
  FEeval l fe1 == FEeval l fe2 ->
-  PCond l (condition nfe1 ++ condition nfe2) ->
+ PCond l (condition nfe1 ++ condition nfe2) ->
  NPphi_pow l np1 ==
  NPphi_pow l np2.
 Proof.
  intros. subst nfe1 nfe2 lmp np1 np2.
- repeat rewrite (Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec).
+ rewrite !(Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec).
  repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl.
- assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)).
- assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)).
- apply (@rmul_reg_l (NPEeval l (rsplit_common den))).
- intro Heq;apply N1.
- rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
- rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq].
- repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))).
- repeat rewrite <- ARth.(ARmul_assoc).
- change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with
-      (NPEeval l (PEmul (rsplit_right den) (rsplit_common den))).
- change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with
-      (NPEeval l (PEmul (rsplit_left den) (rsplit_common den))).
- repeat rewrite <- NPEmul_correct. rewrite <- H3. rewrite <- split_correct_l.
- rewrite <- split_correct_r.
- apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))).
- intro Heq; apply AFth.(AF_1_neq_0).
- rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
- ring [Heq]. rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe2)))).
- repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
- apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
- intro Heq; apply AFth.(AF_1_neq_0).
- rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
- ring [Heq]. repeat rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe1)))).
- repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
- rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
- rewrite  (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
- repeat rewrite <- (AFth.(AFdiv_def)).
- repeat rewrite <- Fnorm_FEeval_PEeval ; trivial.
- apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
+ apply Field_simplify_aux_ok; trivial.
 Qed.
 
 Theorem Field_simplify_eq_in_correct :
@@ -1464,47 +1368,16 @@ forall n l lpe fe1 fe2,
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
  forall den, split (denum nfe1) (denum nfe2) = den ->
- forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 ->
- forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 ->
+ forall np1, Nnorm n lmp (num nfe1 * right den) = np1 ->
+ forall np2, Nnorm n lmp (num nfe2 * left den) = np2 ->
  FEeval l fe1 == FEeval l fe2 ->
-  PCond l (condition nfe1 ++ condition nfe2) ->
- NPphi_dev l np1 ==
- NPphi_dev l np2.
+ PCond l (condition nfe1 ++ condition nfe2) ->
+ NPphi_dev l np1 == NPphi_dev l np2.
 Proof.
  intros. subst nfe1 nfe2 lmp np1 np2.
- repeat rewrite (Pphi_dev_ok Rsth Reqe ARth CRmorph  get_sign_spec).
- repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl.
- assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)).
- assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)).
- apply (@rmul_reg_l (NPEeval l (rsplit_common den))).
- intro Heq;apply N1.
- rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
- rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq].
- repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))).
- repeat rewrite <- ARth.(ARmul_assoc).
- change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with
-      (NPEeval l (PEmul (rsplit_right den) (rsplit_common den))).
- change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with
-      (NPEeval l (PEmul (rsplit_left den) (rsplit_common den))).
- repeat rewrite <- NPEmul_correct;rewrite <- H3. rewrite <- split_correct_l.
- rewrite <- split_correct_r.
- apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))).
- intro Heq; apply AFth.(AF_1_neq_0).
- rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
- ring [Heq]. rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe2)))).
- repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
- apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
- intro Heq; apply AFth.(AF_1_neq_0).
- rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
- ring [Heq]. repeat rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe1)))).
- repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
- rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
- rewrite  (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
- repeat rewrite <- (AFth.(AFdiv_def)).
- repeat rewrite <- Fnorm_FEeval_PEeval;trivial.
- apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
+ rewrite !(Pphi_dev_ok Rsth Reqe ARth CRmorph  get_sign_spec).
+ repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial).
+ apply Field_simplify_aux_ok; trivial.
 Qed.
 
 
@@ -1513,7 +1386,7 @@ Section Fcons_impl.
 Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C).
 
 Hypothesis PCond_fcons_inv : forall l a l1,
-  PCond l (Fcons a l1) ->  ~ NPEeval l a == 0 /\ PCond l l1.
+  PCond l (Fcons a l1) ->  ~ a @ l == 0 /\ PCond l l1.
 
 Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
   match l with
@@ -1521,12 +1394,13 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
   | cons a l1 => Fcons a (Fapp l1 m)
   end.
 
-Lemma fcons_correct : forall l l1,
+Lemma fcons_ok : forall l l1,
   PCond l (Fapp l1 nil) -> PCond l l1.
+Proof.
 induction l1; simpl; intros.
  trivial.
  elim PCond_fcons_inv with (1 := H); intros.
-   destruct l1; auto.
+ destruct l1; trivial. split; trivial. apply IHl1; trivial.
 Qed.
 
 End Fcons_impl.
@@ -1543,21 +1417,15 @@ Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
  end.
 
 Theorem PFcons_fcons_inv:
- forall l a l1, PCond l (Fcons a l1) ->  ~ NPEeval l a == 0 /\ PCond l l1.
-intros l a l1; elim l1; simpl Fcons; auto.
-simpl; auto.
-intros a0 l0.
-generalize (PExpr_eq_semi_correct l a a0); case (PExpr_eq a a0).
-intros H H0 H1; split; auto.
-rewrite H; auto.
-generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
-intros H H0 H1;
- assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)).
-split.
-generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
-apply H0.
-generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
-generalize Hp; case l0; simpl; intuition.
+ forall l a l1, PCond l (Fcons a l1) ->  ~ a @ l == 0 /\ PCond l l1.
+Proof.
+induction l1 as [|e l1]; simpl Fcons.
+- simpl; now split.
+- case PExpr_eq_spec; intros H; rewrite !PCond_cons; intros (H1,H2);
+   repeat split; trivial.
+  + now rewrite H.
+  + now apply IHl1.
+  + now apply IHl1.
 Qed.
 
 (* equality of normal forms rather than syntactic equality *)
@@ -1570,23 +1438,16 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
  end.
 
 Theorem PFcons0_fcons_inv:
- forall l a l1, PCond l (Fcons0 a l1) ->  ~ NPEeval l a == 0 /\ PCond l l1.
-intros l a l1; elim l1; simpl Fcons0; auto.
-simpl; auto.
-intros a0 l0.
-generalize (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th O l nil a a0). simpl.
-  case (Peq ceqb (Nnorm O nil a) (Nnorm O nil a0)).
-intros H H0 H1; split; auto.
-rewrite H; auto.
-generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
-intros H H0 H1;
- assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)).
-split.
-generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
-apply H0.
-generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
-clear get_sign get_sign_spec.
-generalize Hp; case l0; simpl; intuition.
+ forall l a l1, PCond l (Fcons0 a l1) ->  ~ a @ l == 0 /\ PCond l l1.
+Proof.
+induction l1 as [|e l1]; simpl Fcons0.
+- simpl; now split.
+- generalize (ring_correct O l nil a e). lazy zeta; simpl Peq.
+  case Peq; intros H; rewrite !PCond_cons; intros (H1,H2);
+   repeat split; trivial.
+  + now rewrite H.
+  + now apply IHl1.
+  + now apply IHl1.
 Qed.
 
 (* split factorized denominators *)
@@ -1598,42 +1459,36 @@ Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
  end.
 
 Theorem PFcons00_fcons_inv:
-  forall l a l1, PCond l (Fcons00 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
-intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
- intros p H p0 H0 l1 H1.
-   simpl in H1.
-   case (H _ H1); intros H2 H3.
-   case (H0 _ H3); intros H4 H5; split; auto.
-   simpl.
-   apply field_is_integral_domain; trivial.
-   simpl;intros. rewrite pow_th.(rpow_pow_N).
-   destruct (H _ H0);split;auto.
-   destruct n;simpl. apply AFth.(AF_1_neq_0).
-   apply pow_pos_not_0;trivial.
+  forall l a l1, PCond l (Fcons00 a l1) -> ~ a @ l == 0 /\ PCond l l1.
+Proof.
+intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail).
+- intros p H p0 H0 l1 H1.
+  simpl in H1.
+  destruct (H _ H1) as (H2,H3).
+  destruct (H0 _ H3) as (H4,H5). split; trivial.
+  simpl.
+  apply field_is_integral_domain; trivial.
+- intros. destruct (H _ H0). split; trivial.
+  apply PEpow_nz; trivial.
 Qed.
 
 Definition Pcond_simpl_gen :=
-  fcons_correct _ PFcons00_fcons_inv.
+  fcons_ok _ PFcons00_fcons_inv.
 
 
 (* Specific case when the equality test of coefs is complete w.r.t. the
    field equality: non-zero coefs can be eliminated, and opposite can
    be simplified (if -1 <> 0) *)
 
-Hypothesis ceqb_complete : forall c1 c2, phi c1 == phi c2 -> ceqb c1 c2 = true.
+Hypothesis ceqb_complete : forall c1 c2, [c1] == [c2] -> ceqb c1 c2 = true.
 
-Lemma ceqb_rect_complete : forall c1 c2 (A:Type) (x y:A) (P:A->Type),
-  (phi c1 == phi c2 -> P x) ->
-  (~ phi c1 == phi c2 -> P y) ->
-  P (if ceqb c1 c2 then x else y).
+Lemma ceqb_spec' c1 c2 : Bool.reflect ([c1] == [c2]) (ceqb c1 c2).
 Proof.
-intros.
-generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
-generalize (@ceqb_complete c1 c2).
-case (c1 ?=! c2); auto; intros.
-apply X0.
-red; intro.
-absurd (false = true); auto;  discriminate.
+assert (H := morph_eq CRmorph c1 c2).
+assert (H' := @ceqb_complete c1 c2).
+destruct (ceqb c1 c2); constructor.
+- now apply H.
+- intro E. specialize (H' E). discriminate.
 Qed.
 
 Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
@@ -1646,47 +1501,41 @@ Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
  end.
 
 Theorem PFcons1_fcons_inv:
-  forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
-intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
- simpl; intros c l1.
-   apply ceqb_rect_complete; intros.
-  elim (@absurd_PCond_bottom l H0).
-  split; trivial.
-    rewrite <- (morph0 CRmorph); trivial.
- intros p H p0 H0 l1 H1.
-   simpl in H1.
-   case (H _ H1); intros H2 H3.
-   case (H0 _ H3); intros H4 H5; split; auto.
-   simpl.
-   apply field_is_integral_domain; trivial.
- simpl; intros p H l1.
-   apply ceqb_rect_complete; intros.
-  elim (@absurd_PCond_bottom l H1).
-  destruct (H _ H1).
+  forall l a l1, PCond l (Fcons1 a l1) -> ~ a @ l == 0 /\ PCond l l1.
+Proof.
+intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail).
+- simpl; intros c l1.
+  case ceqb_spec'; intros H H0.
+  + elim (@absurd_PCond_bottom l H0).
+  + split; trivial. rewrite <- phi_0; trivial.
+- intros p H p0 H0 l1 H1. simpl in H1.
+  destruct (H _ H1) as (H2,H3).
+  destruct (H0 _ H3) as (H4,H5).
+  split; trivial. simpl. apply field_is_integral_domain; trivial.
+- simpl; intros p H l1.
+  case ceqb_spec'; intros H0 H1.
+  + elim (@absurd_PCond_bottom l H1).
+  + destruct (H _ H1).
     split; trivial.
     apply ropp_neq_0; trivial.
-    rewrite (morph_opp CRmorph) in H0.
-    rewrite (morph1 CRmorph) in H0.
-    rewrite (morph0 CRmorph) in H0.
-    trivial.
- intros;simpl. destruct (H _ H0);split;trivial.
- rewrite pow_th.(rpow_pow_N). destruct n;simpl.
- apply AFth.(AF_1_neq_0). apply pow_pos_not_0;trivial.
+    rewrite (morph_opp CRmorph), phi_0, phi_1 in H0. trivial.
+- intros. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial.
 Qed.
 
-Definition Fcons2 e l := Fcons1 (PExpr_simp e) l.
+Definition Fcons2 e l := Fcons1 (PEsimp e) l.
 
 Theorem PFcons2_fcons_inv:
- forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
+ forall l a l1, PCond l (Fcons2 a l1) -> ~ a @ l == 0 /\ PCond l l1.
+Proof.
 unfold Fcons2; intros l a l1 H; split;
- case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto.
+ case (PFcons1_fcons_inv l (PEsimp a) l1); trivial.
 intros H1 H2 H3; case H1.
-transitivity (NPEeval l a); trivial.
-apply PExpr_simp_correct.
+transitivity (a@l); trivial.
+apply PEsimp_ok.
 Qed.
 
 Definition Pcond_simpl_complete :=
-  fcons_correct _ PFcons2_fcons_inv.
+  fcons_ok _ PFcons2_fcons_inv.
 
 End Fcons_simpl.
 
@@ -1754,22 +1603,22 @@ Hypothesis S_inj : forall x y, 1+x==1+y -> x==y.
 
 Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
 
-Lemma add_inj_r : forall p x y,
+Lemma add_inj_r p x y :
    gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y.
-intros p x y.
+Proof.
 elim p using Pos.peano_ind; simpl; intros.
  apply S_inj; trivial.
  apply H.
    apply S_inj.
-   repeat rewrite (ARadd_assoc ARth).
+   rewrite !(ARadd_assoc ARth).
    rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth); trivial.
 Qed.
 
-Lemma gen_phiPOS_inj : forall x y,
+Lemma gen_phiPOS_inj x y :
   gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y ->
   x = y.
-intros x y.
-repeat rewrite <- (same_gen Rsth Reqe ARth).
+Proof.
+rewrite <- !(same_gen Rsth Reqe ARth).
 case (Pos.compare_spec x y).
  intros.
    trivial.
@@ -1789,9 +1638,10 @@ case (Pos.compare_spec x y).
 Qed.
 
 
-Lemma gen_phiN_inj : forall x y,
+Lemma gen_phiN_inj x y :
   gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
   x = y.
+Proof.
 destruct x; destruct y; simpl; intros; trivial.
  elim gen_phiPOS_not_0 with p.
    symmetry .
@@ -1801,7 +1651,7 @@ destruct x; destruct y; simpl; intros; trivial.
  rewrite gen_phiPOS_inj with (1 := H); trivial.
 Qed.
 
-Lemma gen_phiN_complete : forall x y,
+Lemma gen_phiN_complete x y :
   gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
   N.eqb x y = true.
 Proof.
@@ -1820,31 +1670,22 @@ Section Field.
  Let AFth := F2AF Rsth Reqe Fth.
  Let ARth := Rth_ARth Rsth Reqe Rth.
 
-Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y.
+Lemma ring_S_inj x y : 1+x==1+y -> x==y.
+Proof.
 intros.
-transitivity (x + (1 + - (1))).
- rewrite (Ropp_def Rth).
-   symmetry .
-   apply (ARadd_0_r Rsth ARth).
- transitivity (y + (1 + - (1))).
-  repeat rewrite <- (ARplus_assoc ARth).
-    repeat rewrite (ARadd_assoc ARth).
-    apply (Radd_ext Reqe).
-   repeat rewrite <- (ARadd_comm ARth 1).
-     trivial.
-   reflexivity.
-  rewrite (Ropp_def Rth).
-    apply (ARadd_0_r Rsth ARth).
+rewrite <- (ARadd_0_l ARth x), <- (ARadd_0_l ARth y).
+rewrite <- (Ropp_def Rth 1), (ARadd_comm ARth 1).
+rewrite <- !(ARadd_assoc ARth). now apply (Radd_ext Reqe).
 Qed.
 
-
- Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
+Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
 
 Let gen_phiPOS_inject :=
    gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0.
 
-Lemma gen_phiPOS_discr_sgn : forall x y,
+Lemma gen_phiPOS_discr_sgn x y :
   ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
+Proof.
 red; intros.
 apply gen_phiPOS_not_0 with (y + x)%positive.
 rewrite (ARgen_phiPOS_add Rsth Reqe ARth).
@@ -1857,9 +1698,10 @@ transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y).
  apply (Ropp_def Rth).
 Qed.
 
-Lemma gen_phiZ_inj : forall x y,
+Lemma gen_phiZ_inj x y :
   gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
   x = y.
+Proof.
 destruct x; destruct y; simpl; intros.
  trivial.
  elim gen_phiPOS_not_0 with p.
@@ -1890,9 +1732,10 @@ destruct x; destruct y; simpl; intros.
    reflexivity.
 Qed.
 
-Lemma gen_phiZ_complete : forall x y,
+Lemma gen_phiZ_complete x y :
   gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
   Zeq_bool x y = true.
+Proof.
 intros.
  replace y with x.
  unfold Zeq_bool.