proposition: Lemma identity_morphism r: order r -> order_morphism (identity (substrate r)) r r.
proof: Proof. by move=> or; apply: order_isomorphism_w; apply: identity_is. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)