proposition: Theorem beq_nat_true_iff : forall n1 n2 : nat, beq_nat n1 n2 = true <-> n1 = n2.
proof: Proof. MProof. intros n1 n2. T.split. - apply beq_nat_true. - intros H. rewrite H. rewrite <- beq_nat_refl. T.reflexivity. Qed.