proposition: Lemma nformula_times_nformula_correct : forall (env:PolEnv) (f1 f2 f : NFormula), eval_nformula env f1 -> eval_nformula env f2 -> nformula_times_nformula f1 f2 = Some f -> eval_nformula env f.
proof: Proof. unfold nformula_times_nformula. intros env f1 f2; destruct f1 as [? o]; destruct f2 as [? o0]. case_eq (OpMult o o0) ; simpl ; try discriminate. intros o1 H ? H0 H1 H2. inversion H2 ; simpl. unfold eval_pol. destruct o1; simpl; rewrite (Pmul_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)); apply OpMult_sound with (3:= H);assumption. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl