proposition: Theorem andb_true_elim2 : forall b c : bool, andb b c = true -> c = true.
proof: Proof. Admitted. Theorem plus_1_neq_0' : forall n : nat, (n + 1) =? 0 = false. Proof. intros [|n]. - reflexivity. - reflexivity. Qed.