# Section nat_experiment Variable nat Definition two Definition plus_two

 ``` 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121``` ```Section nat_experiment. Variable a:nat. Definition two := S(S(0)). Definition plus_two(n:nat):nat := S(S(n)). Definition plus_four(n:nat):nat := S(S(S(S(n)))). Lemma appl : plus_two(plus_two(a)) = plus_four(a). Proof. trivial. Qed. Lemma s_appl : S(plus_two(plus_two(a))) = S(plus_four(a)). Proof. trivial. Qed. Lemma dummy : plus_two(two) = plus_four(0). Proof. trivial. Qed. Lemma assoc : S(plus_two(a)) = plus_two(S(a)). Proof. trivial. Qed. 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. End nat_experiment. ```