proposition: Lemma SubON_mono a b : ltA a b <-> ltB (f a) (f b).
proof: Proof. split;intro H. - apply compare_lt_iff in H; apply compare_lt_iff; now rewrite SubON_compare. - apply compare_lt_iff. rewrite <- compare_lt_iff in H. now rewrite SubON_compare in H. Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles) hydras(OrdNotations Schutte_basics)