proposition: Lemma oliftK m (i : 'I_m) : idiv2 (olift i) = i.
proof: Proof. apply/val_eqP; rewrite /= val_idiv2 /= val_olift. by rewrite -divn2 -muln2 -addn1 divnMDl // addn0. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)