proposition: Lemma val_elift m (i : 'I_m) : elift i = i.*2 :> nat.
proof: Proof. case: m i => [[]//|m i]. by rewrite -[LHS]/(i.*2 %% (m.+1 + m.+1)) modn_small // addnn ltn_double. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)