proposition: Lemma OpMult_sound : forall (o o' om: Op1) (x y : R), eval_op1 o x -> eval_op1 o' y -> OpMult o o' = Some om -> eval_op1 om (x * y).
proof: Proof. unfold eval_op1; intros o; destruct o; simpl; intros o' om x y H1 H2 H3. - inversion H3. rewrite H1. now rewrite (Rtimes_0_l sor). - destruct o' ; inversion H3. + rewrite H2. now rewrite (Rtimes_0_r sor). + apply (Rtimes_neq_0 sor) ; auto. - destruct o' ; inversion H3. + rewrite H2; now rewrite (Rtimes_0_r sor). + now apply (Rtimes_pos_pos sor). + apply (Rtimes_nonneg_nonneg sor); [le_less | assumption]. - destruct o' ; inversion H3. + rewrite H2; now rewrite (Rtimes_0_r sor). + apply (Rtimes_nonneg_nonneg sor); [assumption | le_less ]. + now apply (Rtimes_nonneg_nonneg sor). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl