proposition: Lemma idiv2K_even m (i : 'I_(m + m)) : ~~ odd i -> elift (idiv2 i) = i.
proof: Proof. move=> iO. apply/val_eqP; rewrite /= val_elift /= val_idiv2. by rewrite -[X in _ == X]odd_double_half (negPf iO). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)