proposition: Lemma compare_ge_iff (a b: A): le b a <-> compare a b = Gt \/ compare a b = Eq.
proof: Proof. rewrite compare_le_iff, compare_lt_iff, compare_gt_iff, !compare_eq_iff; intuition. Qed.
imports: Coq(Relations RelationClasses Setoid)