proposition: Lemma le_plus : forall x y, x <= y -> exists k, y = k + x.
proof: Proof. induction 1; simpl. ex 0. refl. destruct IHle as [k e]. ex (S k). lia. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)