proposition: Lemma Iff_imp_imp : forall (A B : CProp), (A IFF B) -> (prod (A->B) (B->A)).
proof: Proof. unfold Iff. intuition. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)