proposition: Lemma iso_seg_iso_prop r1 r2 f: order r1 -> order r2 -> iso_seg_iso r1 r2 f -> iso_seg_mor r1 r2(Lf (Vf f) (substrate r1) (substrate r2)).
proof: Proof. move => or1 or2 [ha hb]; move:(proj1 ha) => hc. move: (isomorphism_to_morphism or1 or2 hc hb)=> [qa qb]; split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)