proposition: Lemma pexpr_times_nformula_correct : forall (env: PolEnv) (e: PolC) (f f' : NFormula), eval_nformula env f -> pexpr_times_nformula e f = Some f' -> eval_nformula env f'.
proof: Proof. unfold pexpr_times_nformula. intros env e f; destruct f as [? o]. intros f' H H0. destruct o ; inversion H0 ; try discriminate. simpl in *. unfold eval_pol in *. rewrite (Pmul_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)). rewrite H. apply (Rtimes_0_r sor). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl