proposition: Lemma PP_mult_corr_F : forall (e f:expr) (x y:F), II e x -> II f y -> II (PP_mult 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_mult e2 f) (x[*]y)) -> II (expr_plus e1 e2) x -> II f y -> II (PP_plus (PM_mult f e1) (PP_mult e2 f)) (x[*]y)). cut (forall (i:Z) (f:expr) (x y:F), II (expr_int i) x -> II f y -> II (PM_mult f (expr_int i)) (x[*]y)). cut (forall (e f:expr) (x y:F), II e x -> II f y -> II (expr_mult e f) (x[*]y)). intros H H0 H1 e. elim e; intros; simpl in |- *; auto. intros. apply interpF_mult with x y; algebra. intros. apply interpF_wd with (y[*]x); algebra. apply PM_mult_corr_F; auto. intros. inversion X0. try (rewrite H in X2; rewrite H1 in X3; rewrite H0 in H2). apply interpF_wd with (y[*]x0[+]y0[*]y). apply PP_plus_corr_F; auto. apply PM_mult_corr_F; auto. astepl (x0[*]y[+]y0[*]y). Step_final ((x0[+]y0)[*]y). Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection