proposition: Lemma makeCuttingPlane_ns_sound : forall env e e' c, eval_nformula env (e, NonStrict) -> makeCuttingPlane e = (e',c) -> eval_nformula env (nformula_of_cutting_plane (e', c, NonStrict)).
proof: Proof. unfold nformula_of_cutting_plane. unfold eval_nformula. unfold RingMicromega.eval_nformula. unfold eval_op1. intros env e e' c H H0. rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). simpl. unfold makeCuttingPlane in H0. revert H0. case_eq (Zgcd_pol e) ; intros g c0. generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0). - intros H0 H1 H2. inv H2. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *. apply (Zgcd_pol_correct_lt _ env) in H1. 2: auto using Z.gt_lt. apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r. apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0). apply Z.le_ge. rewrite <- Z.sub_0_l. apply Z.le_sub_le_add_r. rewrite <- H1. assumption. - intros H0 H1 H2. inv H2. auto with zarith. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat