proposition: Lemma order_cp0 r r': order r -> order r' -> ((sub r r') <-> (forall x y, gle r x y -> gle r' x y)).
proof: Proof. move => or or'; split; first by move => h x y xy; apply: h. move => h t tr. move: ((proj41 or) _ tr) => p; move: tr; rewrite -p; apply:h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)