Section nat_experiment. Fixpoint plus (n:nat)(m:nat) : nat := match n with | 0 => m | S(n') => S (plus n' m) end. Fixpoint mult (n:nat)(m:nat) : nat := match n with | 0 => 0 | S(n') => plus m (mult n' m) end. Lemma plus_0_l: forall n:nat, plus 0 n = n. Proof. simpl. reflexivity. Qed. Lemma plus_0_r: forall n:nat, plus n 0 = n. Proof. intros. induction n. reflexivity. simpl. rewrite -> IHn. reflexivity. Qed. Lemma plus_0_r_2: forall n:nat, plus n 0 = n. Proof. intros. destruct n. reflexivity. auto. Qed. Lemma plus_0: forall n:nat, plus n 0 = plus 0 n. Proof. intros. rewrite -> plus_0_l. rewrite -> plus_0_r_2. reflexivity. Qed. Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope. Lemma plus_s: forall n m, n+S(m) = S(n+m). Proof. intros. destruct n. simpl. reflexivity. simpl. auto. Qed. Theorem plus_commutative: forall n m, (plus n m) = (plus m n). Proof. intros n m. induction m. rewrite -> plus_0. reflexivity. simpl. rewrite <- IHm. rewrite <- plus_s. reflexivity. Qed. Theorem plus_associative: forall n m p, (n+m)+p = n+(m+p). Proof. intros n m p. induction n. trivial. simpl. rewrite <- plus_commutative. rewrite <- IHn. rewrite <- plus_commutative. reflexivity. Qed. Lemma plus_ass_com: forall n m p, n + (m+p) = n + (p+m). Proof. intros. induction n. simpl. rewrite -> plus_commutative. reflexivity. simpl. rewrite -> IHn. reflexivity. Qed. Lemma mult_0_r: forall n, mult n 0 = 0. Proof. auto. Qed. Lemma mult_0_l: forall n, mult 0 n = 0. Proof. auto. Qed. Lemma mult_s_l: forall n m, mult (S m) n = n + mult m n. Proof. trivial. Qed. Lemma mult_1_r: forall n, mult n 1 = n. Proof. induction n. rewrite -> mult_0_l. reflexivity. simpl. rewrite IHn. reflexivity. Qed. Lemma mult_s_r: forall n m, mult n (S m) = n + mult n m. Proof. intros n m. induction n. rewrite -> mult_0_l. rewrite -> mult_0_l. simpl. reflexivity. simpl. rewrite -> IHn. rewrite -> plus_commutative. rewrite -> plus_associative. rewrite -> plus_ass_com. reflexivity. Qed. Theorem mult_commutative: forall n m, (mult n m) = (mult m n). Proof. intros. induction n. rewrite -> mult_0_r. rewrite -> mult_0_l. reflexivity. rewrite -> mult_s_l. rewrite -> IHn. rewrite -> mult_s_r. reflexivity. Qed. End nat_experiment.