proposition: Theorem plus_n_O_firsttry : forall n:nat, n = n + 0.
proof: Proof. MProof. intros n. simpl. Abort. Theorem plus_n_O_secondtry : forall n:nat, n = n + 0. MProof. intros n. destruct n &> [i: ~~ | \n']. - reflexivity. - simpl. Abort. Theorem plus_n_O : forall n:nat, n = n + 0. MProof. intros n. elim n &> [i: ~~ | \n' IHn']. - reflexivity. - simpl. rewrite <- IHn'. reflexivity. Qed.