beka valentine on Nostr: Lemma plus_assoc_2 : forall (m n p : Nat), plus m (plus n p) = plus (plus m n) p. ...

Lemma plus_assoc_2 : forall (m n p : Nat), plus m (plus n p) = plus (plus m n) p.
Proof.
intros.
induction m.
-
simpl.
reflexivity.
-
simpl.
f_equal.
exact IHm.
Qed.