proposition: Lemma mul_n_Sm : forall n m:nat, n * m + n = n * S m.
proof: Proof. intros; simple_induction n p H; simpl; auto. destruct H; rewrite <- add_n_Sm; apply ap. pattern m at 1 3; elim m; simpl; auto. Defined.
imports: Basics Types Basics.Nat HoTT.DProp