proposition: Lemma monotonic_switch_step_it_odd l c (ts : l.*2.+1.-tuple _) : edom c \subset edom (switch_step_it (switch c) ts) /\ {in edom c, edges (switch_step_it (switch c) ts) =1 edges c}.
proof: Proof. rewrite (tuple_eta ts) /=. have Hbe: size (behead ts) == l.*2. by rewrite size_behead size_tuple. have -> : behead ts = Tuple Hbe by []. rewrite /edom -(conodes_switch_nodes c). split. rewrite (subset_trans _ (proj1 (monotonic_switch_step_it _ (Tuple Hbe)))) /edom //=. by rewrite (subset_trans _ (monotonic_codom_step_it _ _)). move=> p Hp. rewrite (proj2 (monotonic_switch_step_it _ _)). rewrite monotonic_switch_edges_step_it //. by rewrite switchK_edges. rewrite /edom /=. apply/subsetP: Hp. by apply monotonic_codom_step_it. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner