proposition: Lemma sub_numeration r f x: let r' := induced_order r (segment r x) in worder r -> numeration r f -> inc x (substrate r) -> numeration r' (restr f (segment r x)).
proof: Proof. move=> r' wor num xsr. have sss:= (@sub_segment r x). have wor':=(induced_wor wor sss). have [fgf df pf]:= num. have sr':substrate r' = (segment r x) by rewrite /r' iorder_sr; fprops. have ssd: sub (segment r x) (domain f) by ue. have dr:domain (restr f (segment r x)) = substrate r' by aw. split; aww => a asr. have sra: (segment r' a = segment r a). apply: segment_induced_a =>//; fprops. apply: segment_segment; fprops. rewrite sra (restr_ev _ asr) pf; last by apply:ssd. have ssad: sub (segment r a) (domain f) by rewrite df; apply:sub_segment. have sax: sub (segment r a) (segment r x). move=> t; move: asr => /segmentP p1 /segmentP p2. have or: order r by fprops. apply /segmentP;order_tac. apply: direct_image_exten; aww. by move=> z zs; rewrite restr_ev => //; apply: sax. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)