proposition: Lemma freeon_trans d m0 n0 (m0n0 : n0 \in 'V m0) d' t (Ht : freeon ('V m0 :\ n0) d d') : freeon (`V(m0, n0) :\ n0) d t -> freeon (`V(m0, n0) :\ n0) d' t.
proof: Proof. move=> Hlhs2. apply/forallP => /= n1. rewrite in_setD1 negb_and negbK. apply/implyP => /orP[/eqP ->{n1}|]. rewrite -(freeon_notin Hlhs2) ?in_setD1 ?eqxx //. by rewrite (freeon_notin Ht) // !inE eqxx. move=> Hn1. rewrite -(freeon_notin Hlhs2) ?in_setD1 ?(negbTE Hn1) ?andbF //. rewrite (freeon_notin Ht) //. apply: contra Hn1 => Hn1. move/Fnext_Vnext_Vgraph : m0n0. move/subsetP/(_ _ Hn1). rewrite in_setD1. by case/andP. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR Reals_ext f2 summary subgraph_partition tanner tanner_partition fdist channel checksum