proposition: Lemma MM_mult_corr_F : forall (e f:expr) (x y:F), II e x -> II f y -> II (MM_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 (MM_mult e2 f) (x[*]y)) -> II (expr_mult e1 e2) x -> II f y -> II (MV_mult (MM_mult e2 f) e1) (x[*]y)). cut (forall (i:Z) (f:expr) (x y:F), II (expr_int i) x -> II f y -> II (MI_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 MI_mult_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 MV_mult_corr_F; auto. astepl (x0[*](y0[*]y)). Step_final (x0[*]y0[*]y). Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection