proposition: Lemma PM_mult_corr_R : forall (e f:expr) (x y:R), II e x -> II f y -> II (PM_mult 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_mult e2 f) (x[*]y)) -> II (expr_plus e1 e2) x -> II f y -> II (PM_plus (PM_mult e2 f) (MM_mult e1 f)) (x[*]y)). cut (forall (i:Z) (f:expr) (x y:R), II (expr_int i) x -> II f y -> II (PM_plus (expr_int 0) (MI_mult f (expr_int i))) (x[*]y)). cut (forall (e f:expr) (x y:R), 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 interpR_mult with x y; algebra. intros. apply interpR_wd with (zring 0[+]y[*]x). apply PM_plus_corr_R. apply interpR_int; algebra. apply MI_mult_corr_R; auto. astepl ([0][+]y[*]x). Step_final (y[*]x). intros. inversion X0. try (rewrite H in X2; rewrite H1 in X3; rewrite H0 in H2). apply interpR_wd with (y0[*]y[+]x0[*]y). apply PM_plus_corr_R; auto. apply MM_mult_corr_R; auto. astepl ((y0[+]x0)[*]y). Step_final ((x0[+]y0)[*]y). Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection