12 lines
288 B
Coq
12 lines
288 B
Coq
Lemma transparent_plus_zero: forall n, n + O = n.
|
|
intros n; induction n.
|
|
- reflexivity.
|
|
- simpl; rewrite IHn; trivial.
|
|
Defined.
|
|
|
|
Lemma transparent_plus_S: forall n m, n + S m = S n + m .
|
|
intros n; induction n; intros m.
|
|
- reflexivity.
|
|
- simpl; f_equal; rewrite IHn; reflexivity.
|
|
Defined.
|