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