proposition: Lemma MV_mult_corr_R : forall (e f:expr) (x y:R), II e x -> II f y -> II (MV_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 (MV_mult e2 f) (x[*]y)) -> II (expr_mult e1 e2) x -> II f y -> II (expr_mult e1 (MV_mult e2 f)) (x[*]y)). cut (forall (e f:expr) (x y:R), II e x -> II f y -> II (MI_mult (expr_mult f expr_one) e) (x[*]y)). cut (forall (e f:expr) (x y:R), II e x -> II f y -> II (expr_mult f e) (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 H2 e. elim e. simpl in |- *; auto. simpl in |- *; auto. intros e1 H3 e2 H4. elim e1; simpl in |- *; auto. intros e1 H3 e2 H4. elim e1; simpl in |- *; auto. intros n f. elim f; simpl in |- *; auto. intro m. elim (lt_nat n m); simpl in |- *; auto. intros u e0 H5 f. elim f; simpl in |- *; auto. intros u0 e3 H6. elim lt_nat; simpl in |- *; auto. elim andb; simpl in |- *; auto. intros b e0 H6 e3 H7 f. elim f; simpl in |- *; auto. intros b0 e4 H8 e5 H9. elim lt_nat; simpl in |- *; auto. elim andb; simpl in |- *; auto. elim andb; simpl in |- *; auto. intros n f H5 f0. elim f0; simpl in |- *; auto. intros f1 e0 H6. elim lt_nat; simpl in |- *; auto. elim andb; simpl in |- *; auto. intros. inversion X1. intros n e0 H3 f. elim f; simpl in |- *; auto. intros n e0 H3 e1 H4 f. elim f; simpl in |- *; auto. intros n e0 H3 f. elim f; simpl in |- *; auto. intros; apply interpR_mult with x y; algebra. intros; apply interpR_wd with (y[*]x); algebra. apply interpR_mult with y x; algebra. intros; apply interpR_wd with (y[*][1][*]x). apply MI_mult_corr_R; auto. apply interpR_mult with y ([1]:R); algebra. apply (interpR_int R val unop binop pfun 1); algebra. Step_final (x[*](y[*][1])). intros. inversion X0. try (rewrite H0 in H2; rewrite H in X2; rewrite H1 in X3). apply interpR_wd with (x0[*](y0[*]y)). apply interpR_mult with x0 (y0[*]y); algebra. Step_final (x0[*]y0[*]y). Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection