proposition: Lemma prl_exa3_prop1: [/\ preorder r, substrate r = Nat & forall i j, gle r i j <-> [/\ natp i, natp j & i <=c j]].
proof: Proof. move:Nat_order_wor => [[/order_preorder ha _] hb]; split => //. exact:Nat_order_leP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)