proposition: Lemma OpAdd_sound : forall (o o' oa : Op1) (e e' : R), eval_op1 o e -> eval_op1 o' e' -> OpAdd o o' = Some oa -> eval_op1 oa (e + e').
proof: Proof. unfold eval_op1; intros o; destruct o; simpl; intros o' oa e e' H1 H2 Hoa. - inversion Hoa as [H0]. rewrite <- H0. destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor). - destruct o'. + inversion Hoa. rewrite H2. now rewrite (Rplus_0_r sor). + discriminate. + discriminate. + discriminate. - destruct o'. + inversion Hoa. rewrite H2. now rewrite (Rplus_0_r sor). + discriminate. + inversion Hoa. now apply (Rplus_pos_pos sor). + inversion Hoa. now apply (Rplus_pos_nonneg sor). - destruct o'. + inversion Hoa. now rewrite H2, (Rplus_0_r sor). + discriminate. + inversion Hoa. now apply (Rplus_nonneg_pos sor). + inversion Hoa. now apply (Rplus_nonneg_nonneg sor). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl