proposition: Lemma PM_plus_corr_R : forall (e f:expr) (x y:R), II e x -> II f y -> II (PM_plus e f) (x[+]y).
proof: Proof. cut (forall (e1 e2 f:expr) (x y:R), (forall (f:expr) (x y:R), II e2 x -> II f y -> II (PM_plus e2 f) (x[+]y)) -> II (expr_plus e1 e2) x -> II f y -> II (expr_plus e1 (PM_plus e2 f)) (x[+]y)). cut (forall (e1 e2 f:expr) (x y:R), (forall (f:expr) (x y:R), II e2 x -> II f y -> II (PM_plus e2 f) (x[+]y)) -> II (expr_plus e1 e2) x -> II f y -> II (PM_plus e2 (MM_plus e1 f)) (x[+]y)). cut (forall (e f:expr) (x y:R), II e x -> II f y -> II (MM_plus e f) (x[+]y)). cut (forall (e f:expr) (x y:R), II e x -> II f y -> II (expr_plus e f) (x[+]y)). cut (forall (e f:expr) (x y:R), II e x -> II f y -> II (expr_plus f e) (x[+]y)). intros H H0 H1 H2 H3 e. elim e. simpl in |- *; auto. intros z f; elim f; intros; simpl in |- *; auto. intros e1 H4 e2 H5 f. simpl in |- *. elim (lt_monom e1 f); elim (eq_monom e1 f); elim f; intros; simpl in |- *; auto. simpl in |- *; auto. simpl in |- *; auto. simpl in |- *; auto. simpl in |- *; auto. simpl in |- *; auto. intros; apply interpR_wd with (y[+]x); algebra. apply interpR_plus with y x; algebra. intros; apply interpR_plus with x y; algebra. intros; apply MM_plus_corr_R; auto. intros. inversion X0. try (rewrite H in X2; rewrite H1 in X3; rewrite H0 in H2). apply interpR_wd with (y0[+](x0[+]y)). apply X; auto. apply MM_plus_corr_R; auto. astepl (y0[+]x0[+]y). Step_final (x0[+]y0[+]y). intros. inversion X0. try (rewrite H in X2; rewrite H1 in X3; rewrite H0 in H2). apply interpR_wd with (x0[+](y0[+]y)). apply interpR_plus with x0 (y0[+]y); algebra. Step_final (x0[+]y0[+]y). Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection