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