proposition: Lemma le_witness : forall x y : nat, x <= y -> exists q : nat, x + q = y.
proof: Proof. intros x y. intro. elim H. split with 0. simpl in |- *. symmetry in |- *. apply plus_n_O. intros. case H1. intros. split with (S x0). replace (x + S x0) with (S (x + x0)). simpl in |- *. rewrite H2. reflexivity. apply plus_n_Sm. Qed.
imports: ZArith EqNat