proposition: Lemma sub_order_r: order_r sub.
proof: Proof. split. + by move=> x y t xy yz; apply: (sub_trans xy yz). + by move=> x y xy yx; apply: extensionality. + by move=> x y; split; apply: sub_refl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)