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