fact: Definition rhalf_cleaner_rec n : network (`2^ n) := if n is n1.+1 then rhalf_cleaner (`2^ n1) :: ndup (half_cleaner_rec false n1) else [::].
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort