proposition: Lemma Iff_trans : forall (A B C : CProp), (prod (A IFF B) (B IFF C)) -> (A IFF C).
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)