proposition: Lemma identity_is r: order r -> order_isomorphism (identity (substrate r)) r r.
proof: Proof. move=> or; hnf; rewrite /fiso_prop; aw; trivial;split => //. saw;apply: identity_fb. move=> x t xsr ysr; rewrite ? idV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)