proposition: Theorem double_injective_FAILED : forall n m, double n = double m -> n = m.
proof: Proof. intros n m. induction n as [| n' IHn']. - simpl. intros eq. destruct m as [| m'] eqn:E. + reflexivity. + discriminate eq. - intros eq. destruct m as [| m'] eqn:E. + discriminate eq. + apply f_equal. Abort. Theorem double_injective : forall n m, double n = double m -> n = m. Proof. intros n. induction n as [| n' IHn']. - simpl. intros m eq. destruct m as [| m'] eqn:E. + reflexivity. + discriminate eq. - intros m eq. destruct m as [| m'] eqn:E. + discriminate eq. + apply f_equal. apply IHn'. simpl in eq. injection eq as goal. apply goal. Qed.