proposition: Lemma lt_unique : forall n m (h1 h2 : n < m), h1 = h2.
proof: Proof. intros n m. unfold lt. intros. apply le_unique. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)