proposition: Lemma PP_plus_corr_F : forall (e f:expr) (x y:F), II e x -> II f y -> II (PP_plus e f) (x[+]y).
proof: Proof. cut (forall (e1 e2 f:expr) (x y:F), (forall (f:expr) (x y:F), II e2 x -> II f y -> II (PP_plus e2 f) (x[+]y)) -> II (expr_plus e1 e2) x -> II f y -> II (PM_plus (PP_plus e2 f) e1) (x[+]y)). cut (forall (i:Z) (f:expr) (x y:F), II (expr_int i) x -> II f y -> II (PM_plus f (expr_int i)) (x[+]y)). cut (forall (e f:expr) (x y:F), II e x -> II f y -> II (expr_plus e f) (x[+]y)). intros H H0 H1 e. elim e; intros; simpl in |- *; auto. intros. apply interpF_plus with x y; algebra. intros. apply interpF_wd with (y[+]x); algebra. apply PM_plus_corr_F; auto. intros. inversion X0. try (rewrite H in X2; rewrite H1 in X3; rewrite H0 in H2). apply interpF_wd with (y0[+]y[+]x0). apply PM_plus_corr_F; auto. astepl (x0[+](y0[+]y)). Step_final (x0[+]y0[+]y). Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection