proposition: Lemma numeration_unique r f f': worder r -> numeration r f -> numeration r f' -> f = f'.
proof: Proof. move=> [or wor] [fgf df Vf][fgf' df' Vf']. set A :=Zo (substrate r)(fun x=> Vg f x <> Vg f' x). case: (emptyset_dichot A)=> neA. apply: (fgraph_exten fgf fgf'); rewrite df => // a xdf. by ex_middle nVV; empty_tac1 a; apply: Zo_i. have sAs: sub A (substrate r) by apply: Zo_S. move: (wor _ sAs neA)=> [y []]; rewrite iorder_sr // => yA leyA. move: (sAs _ yA)=> ysr. have srp: forall z, inc z (segment r y) -> Vg f z = Vg f' z. move=> z /segmentP zy; ex_middle nVV. have zA: (inc z A) by apply: Zo_i=>//; order_tac. move: (iorder_gle1 (leyA _ zA)) => yz; order_tac. have nyA: Vg f y = Vg f' y. rewrite df in Vf; rewrite df' in Vf'. rewrite Vf // Vf' //. apply: direct_image_exten =>//. rewrite df; apply: sub_segment. rewrite df'; apply: sub_segment. by move: yA => /Zo_P [_ []]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)