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