proposition: Lemma witness_le : forall x y : nat, (exists q : nat, x + q = y) -> x <= y.
proof: Proof. intros. elim H. intro q. intros. rewrite <- H0. elim q. rewrite <- plus_n_O. apply le_n. intros. rewrite <- plus_n_Sm. apply le_S. assumption. Qed.
imports: ZArith EqNat