I've figured it out. Not pretty, but it does work.
Lemma plus_0 : forall x, x + 0 = x.
Proof.
induction x.
- reflexivity.
- simpl. rewrite IHx. reflexivity.
Qed.
Lemma plus_comm : forall a b, a + b = b + a.
Proof.
induction a.
- intro b. rewrite plus_0. reflexivity.
- intro b. rewrite <- plus_n_Sm. rewrite <- IHa. reflexivity.
Qed.
Lemma plus_assoc : forall a b c, a + b + c = a + (b + c).
Proof.
induction a.
- reflexivity.
- intros b c. simpl. rewrite IHa. reflexivity.
Qed.
Lemma mul_dist : forall k x y, k * (x + y) = k * x + k * y.
Proof.
induction k.
- intros x y. reflexivity.
- intros x y. simpl. rewrite IHk.
replace (k*x+k*y) with (k*y+k*x).
rewrite <- plus_assoc.
replace (x+y+k*y) with (x + (y+k*y)).
replace (y + k * y) with (S k * y).
rewrite plus_comm.
rewrite <- plus_assoc.
replace (k*x+x) with (x+k*x).
reflexivity.
+ rewrite plus_comm. reflexivity.
+ reflexivity.
+ rewrite plus_assoc. rewrite plus_comm. reflexivity.
+ rewrite plus_comm. reflexivity.
Qed.
Lemma times_0 : forall a, a * 0 = 0.
Proof.
induction a.
- reflexivity.
- simpl. rewrite IHa. reflexivity.
Qed.
Lemma mul_comm : forall a b, a * b = b * a.
Proof.
induction a.
- intro b. rewrite times_0. reflexivity.
- intro b. rewrite <- mult_n_Sm. rewrite <- IHa.
rewrite plus_comm. reflexivity.
Qed.
Lemma mul_assoc : forall a b c, a * b * c = a * (b * c).
Proof.
induction a.
- reflexivity.
- intros b c. simpl. rewrite <- IHa.
rewrite mul_comm. rewrite mul_dist.
replace (c * (a * b)) with (a * b * c). rewrite mul_comm. reflexivity.
+ rewrite mul_comm. reflexivity.
Qed.
Lemma principal : forall x, 6 * x = 3 * (2 * x).
Proof.
intro x. replace 6 with (3 * 2). rewrite mul_assoc. reflexivity.
- reflexivity.
Qed.
