proposition: Lemma order_reflexivityP r: order r -> forall a, (inc a (substrate r) <-> gle r a a).
proof: Proof. move=> [_ or _ _]; rewrite /gle;split => h; [by apply: or | substr_tac]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)