proposition: Lemma gt_plus : forall l k, l > k -> exists m, l = (m + 1) + k.
proof: Proof. induction 1. exists 0. lia. destruct IHle. exists (S x). lia. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)