proposition: Theorem eqb_true : forall n m, n =? m = true -> n = m.
proof: Proof. Admitted. Definition manual_grade_for_informal_proof : option (nat*string) := None. Theorem plus_n_n_injective : forall n m, n + n = m + m -> n = m. Proof. Admitted. Theorem double_injective_take2_FAILED : forall n m, double n = double m -> n = m. Proof. intros n m. induction m as [| m' IHm']. - simpl. intros eq. destruct n as [| n'] eqn:E. + reflexivity. + discriminate eq. - intros eq. destruct n as [| n'] eqn:E. + discriminate eq. + apply f_equal. Abort. Theorem double_injective_take2 : forall n m, double n = double m -> n = m. Proof. intros n m. generalize dependent n. induction m as [| m' IHm']. - simpl. intros n eq. destruct n as [| n'] eqn:E. + reflexivity. + discriminate eq. - intros n eq. destruct n as [| n'] eqn:E. + discriminate eq. + apply f_equal. apply IHm'. injection eq as goal. apply goal. Qed.