proposition: Lemma eq_Rnorm invb R (f f' : R -> F) (e : RExpr R) : f =1 f' -> Rnorm invb f e = Rnorm invb f' e.
proof: Proof. pose P R e := forall invb (f f' : R -> F), f =1 f' -> Rnorm invb f e = Rnorm invb f' e. pose P0 V e := forall invb (f f' : V -> F), f =1 f' -> Mnorm invb f e = Mnorm invb f' e. move: invb f f'; elim e using (@RExpr_ind' P P0); rewrite {R e}/P {}/P0 //=. - move=> R e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - move=> e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - move=> e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - move=> e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - by move=> R e1 IHe1 e2 _ invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> R e1 IHe1 invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> e1 IHe1 invb f f' feq; rewrite (IHe1 _ _ _ feq). - move=> e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - by move=> R e1 IHe1 e2 _ invb f f' feq; rewrite (IHe1 _ _ _ feq). - move=> R e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - move=> e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - move=> e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - move=> e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - by move=> R e1 IHe1 n invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> R e1 IHe1 n invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> R e1 IHe1 n invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> e1 IHe1 n invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> e1 IHe1 n invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> e1 IHe1 [|p|p] invb f f' feq //; rewrite (IHe1 _ _ _ feq). - by move=> R e1 IHe1 invb f f' feq; rewrite !(IHe1 _ _ _ feq). - by move=> P e1 IHe1 invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> S R g e1 IHe1 invb f f' feq; apply: IHe1 => x; apply: feq. - by move=> V R g e1 IHe1 invb f f' feq; apply: IHe1 => x; apply: feq. - by move=> R g e1 _ invb f f' ->. - by move=> R g e1 _ invb f f' ->. - by move=> R g e1 _ invb f f' ->. - by move=> R g e1 _ invb f f' ->. - by move=> R x invb f f' ->. - move=> V e1 IHe1 e2 IHe2 invb f f' feq. by rewrite (IHe1 _ _ _ feq) (IHe2 _ _ _ feq). - by move=> V e1 IHe1 e2 _ invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> V e1 IHe1 invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> V e1 IHe1 e2 _ invb f f' feq; rewrite (IHe1 _ _ _ feq). - by move=> U V g e1 IHe1 invb f f' feq; apply: IHe1 => x; apply: feq. - by move=> V g e1 _ invb f f' ->. - by move=> V g e1 _ invb f f' ->. - by move=> V g e1 _ invb f f' ->. - by move=> V g e1 _ invb f f' ->. - by move=> V x invb f f' ->. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)