proposition: Lemma beq_nat_eq : forall n m : nat, n = m <-> beq_nat n m = true.
proof: Proof. simple induction n. intro. case m. simpl in |- *. split. reflexivity. reflexivity. simpl in |- *. split. intro. discriminate. intro. discriminate. intros n1 IH. intro m. case m. simpl in |- *. split. intro. discriminate. intro. discriminate. intro m1. intros. simpl in |- *. elim (IH m1). split. intro. injection H1. assumption. intros. rewrite H0. reflexivity. assumption. Qed.
imports: Arith ZArith EqNat