proposition: Lemma compare_le_iff (a b: A): le a b <-> compare a b = Lt \/ compare a b = Eq.
proof: Proof. split; intro H. - apply le_lt_eq in H as [Hlt | Heq]. * left; now apply compare_lt_iff. * right; now apply compare_eq_iff. - apply le_lt_eq; destruct H as [Hlt | Heq]. * left; now apply compare_lt_iff. * right; now apply compare_eq_iff in Heq. Qed.
imports: Coq(Relations RelationClasses Setoid)