proposition: Lemma blt_nat_ok : forall x y, blt_nat x y = true <-> x < y.
proof: Proof. intros. unfold blt_nat. rewrite bgt_nat_ok. lia. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)