proposition: Lemma lt_witness : forall x y : nat, x < y -> exists q : nat, x + q = y /\ 0 < q.
proof: Proof. unfold lt in |- *. intros. elim (le_witness (S x) y). intros. split with (S x0). split. rewrite <- plus_n_Sm. assumption. apply le_n_S. apply le_O_n. assumption. Qed.
imports: ZArith EqNat