proposition: Theorem test_acyclic : forall p, p \in [::] :: mypath (m+n) -> (size p > 2) ==> ~~ ucycleb myrel p.
proof: Proof. by apply /allP. Qed.
imports: Wf_nat Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2 fdist channel pproba linearcode subgraph_partition tanner tanner_partition summary ldpc checksum ldpc_algo