proposition: Lemma lt_not_ge (a b: A): lt a b -> ~ le b a.
proof: Proof. intros Hlt Hle. apply le_lt_eq in Hle as [Hgt | Heq]. - now apply lt_not_gt in Hlt. - subst; now apply StrictOrder_Irreflexive in Hlt. Qed.
imports: Coq(Relations RelationClasses Setoid)