proposition: Lemma lt_exist : forall m n, m < n -> { p | m + p = n }.
proof: Proof. intro m ; induction m ; intros n mltn. exists n ; trivial. destruct n as [| n] ; [exfalso ; lia |] ; destruct (IHm n (proj2 (Nat.succ_lt_mono m n) mltn)) as [p Hp] ; exists p ; intuition lia. Qed.
imports: Arith Lia