proposition: Lemma cflip_default m (clink : {ffun 'I_m -> 'I_m}) (b : bool) : [forall i, [ffun => b] (clink i) == [ffun => b] i].
proof: Proof. by apply/forallP=> i; rewrite !ffunE. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple