proposition: Lemma sub_connector A B n m (p : 'I_m -> pathS G) : n <= m -> connector A B p -> exists q : 'I_n -> pathS G, connector A B q.
proof: Proof. move => n_leq_m conn_p. pose W := widen_ord n_leq_m. exists (fun i => p (W i)). case: conn_p => C1 C2 C3 C4. split => // i j. exact:(C4 (W i) (W j)). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)