proposition: Lemma lt_ge_dec x y : {x < y} + {x >= y}.
proof: Proof. destruct (lt_eq_lt_dec x y); auto; try destruct s; auto with *. Defined.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)