proposition: Lemma CNot_Not_or : forall A B C : CProp, (A -> Not C) -> (B -> Not C) -> ~ Not (A or B) -> Not C.
proof: Proof. intros A B C H H0 H1. intro H2. apply H1. intro H3. elim H3. intro; apply H; auto. intro; apply H0; auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)