proposition: Lemma genCuttingPlaneNone : forall env f, genCuttingPlane f = None -> eval_nformula env f -> False.
proof: Proof. unfold genCuttingPlane. intros env f; destruct f as [p o]. destruct o. - case_eq (Zgcd_pol p) ; intros g c. case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))). + intros H H0 H1 H2. flatten_bool. match goal with [ H' : (g >? 0) = true |- ?G ] => rename H' into H3 end. match goal with [ H' : negb (Zeq_bool c 0) = true |- ?G ] => rename H' into H end. match goal with [ H' : negb (Zeq_bool (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end. rewrite negb_true_iff in H5. apply Zeq_bool_neq in H5. rewrite <- Zgt_is_gt_bool in H3. rewrite negb_true_iff in H. apply Zeq_bool_neq in H. change (eval_pol env p = 0) in H2. rewrite Zgcd_pol_correct_lt with (1:= H0) in H2. 2: auto using Z.gt_lt. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) in *; clearbody x. contradict H5. apply Zis_gcd_gcd. * apply Z.lt_le_incl, Z.gt_lt; assumption. * constructor; auto with zarith. exists (-x). rewrite Z.mul_opp_l, Z.mul_comm. now apply Z.add_move_0_l. + destruct (makeCuttingPlane p); discriminate. - discriminate. - destruct (makeCuttingPlane (PsubC Z.sub p 1)) ; discriminate. - destruct (makeCuttingPlane p) ; discriminate. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat