proposition: Lemma or_not_and : forall (A : CProp) (B : Prop), Not A \/ ~ B -> Not (A and B).
proof: Proof. intros. intro H0. elim H0. intros. case H. intro H3. apply H3. assumption. intro H3. apply H3. assumption. Qed.
imports: CoRN.reals.Q_in_CReals