proposition: Lemma le_diff0 : forall b a c : nat, a <= b -> a = b + c -> c = 0.
proof: Proof. simple induction b. simpl in |- *. intro. case a. intros. rewrite H0. reflexivity. intros. elim (lt_n_O n). assumption. intros b1 IH. simpl in |- *. intros. rewrite H0 in H. apply (IH (b1 + c) c). apply le_S_n. assumption. reflexivity. Qed.
imports: ZArith EqNat