proposition: Lemma eqb_spec_false x y : eqb x y = false <-> x <> y.
proof: Proof. split. - intros H1 H2. subst y. rewrite eqb_refl in H1. inversion H1. - intro H. case_eq (eqb x y); auto. intro H1. elim H. now rewrite <- eqb_spec. Qed.
imports: Bool OrderedType