proposition: Lemma minus_minus_lem2 : forall a b : nat, b <= a -> a - (a - b) = b.
proof: Proof. simple induction b. intros. elim minus_n_O. elim minus_n_n. trivial with arith. intros. replace (a - (a - S n)) with (S a - S (a - S n)). rewrite <- (minus_Sn_m a (S (a - S n))). rewrite (minus_Sn_m a (S n)). simpl in |- *. rewrite <- H. rewrite H. rewrite H. trivial with arith. apply le_Sn_le. exact H0. apply le_Sn_le. exact H0. apply le_Sn_le. exact H0. exact H0. rewrite minus_Sn_m. simpl in |- *. apply minus_le_lem2. exact H0. simpl in |- *. trivial with arith. Qed.
imports: Plus Mult Minus Lt Le Gt