proposition: Lemma SubON_inj : forall a b, f a = f b -> a = b.
proof: Proof. intros a b H; apply compare_eq_iff; apply compare_eq_iff in H; now rewrite SubON_compare in H. Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles) hydras(OrdNotations Schutte_basics)