proposition: Theorem mult_S_1 : forall n m : nat, m = S n -> m * (1 + n) = m * m.
proof: Proof. MProof. Admitted. Theorem plus_1_neq_0_firsttry : forall n : nat, beq_nat (n + 1) 0 = false. MProof. intros n. simpl. Abort. Theorem plus_1_neq_0 : forall n : nat, beq_nat (n + 1) 0 = false. MProof. intros n. destruct n &> [i: ~~ | \n']. - reflexivity. - reflexivity. Qed.