proposition: Theorem def_mul_mul : forall n m, n ** m == n * m.
proof: Proof. intros n m; induct m. - now rewrite def_mul_0_r, mul_0_r. - intros m IH; now rewrite def_mul_succ_r, mul_succ_r, def_add_add, IH. Qed.
imports: Bool RelationPairs NStrongRec