proposition: Lemma order_leR x: order x -> x <=O x.
proof: Proof. move=> ox; split => //; exists (identity (substrate x)), (substrate x). have ss:= (@sub_refl (substrate x)). have [pa pb]:=(iorder_osr ox ss). by rewrite (iorder_substrate ox); split => //;apply:identity_is. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)