proposition: Lemma conv_incr' A B (x y: X A B): x` <== y` -> x <== y.
proof: Proof. intro H. rewrite <- (conv_invol x). rewrite <- (conv_invol y). apply conv_incr; exact H. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing)