proposition: Theorem def_add_add : forall n m, n +++ m == n + m.
proof: Proof. intros n m; induct n. - now rewrite def_add_0_l, add_0_l. - intros n H. now rewrite def_add_succ_l, add_succ_l, H. Qed.
imports: Bool RelationPairs NStrongRec