proposition: Lemma monotonic_step_rel : subrel (graph_rel c) (graph_rel c').
proof: Proof. rewrite /graph_rel => x y. destruct x,y. destruct g, g0, b, b0 => //. - move/existsP => [s1] /and4P[Hs Hos Ho0s Hoo0]. apply/existsP; exists s1; rewrite Hos Ho0s Hoo0 /= /step_nodes. by case: ifP; rewrite Hs. - move/andP => [Hod Heo]. rewrite (subsetP monotonic_edom_step _ Hod). by rewrite monotonic_edges_step. - move/andP => [Hod Heo]. rewrite (subsetP monotonic_edom_step _ Hod). by rewrite monotonic_edges_step. - move/existsP => [s1] /and4P[Hs Hos Ho0s Hoo0]. apply/existsP; exists s1; rewrite Hos Ho0s Hoo0 /= /step_conodes. case: Bool.bool_dec => Htriv. case: ifP => Hcond /=. by rewrite inE Hs orbT. by rewrite Hs. by rewrite Hs. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner