proposition: Lemma eqb_eq : forall x y, eqb x y = true <-> x==y.
proof: Proof. unfold eqb. intros x y. destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate. - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). Qed.
imports: Relations Morphisms Setoid Equalities