proposition: Theorem eqb_false_iff : forall (A : Set)(eqd : EqDec A)(a1 a2 : A), eqb a1 a2 = false <-> a1 <> a2.
proof: Proof. intuition. subst. rewrite eqb_refl in H. discriminate. case_eq (eqb a1 a2); intuition. rewrite eqb_leibniz in H0. intuition. Qed.
imports: Bvector Arith