proposition: Lemma val_idiv2 m (i : 'I_(m + m)) : idiv2 i = i./2 :> nat.
proof: Proof. case: m i => [[]//|n i /=]. rewrite modn_small // -ltn_double -[X in _ < X]addnn. rewrite (leq_ltn_trans _ (ltn_ord i)) //. by rewrite -[X in _ <= X]odd_double_half leq_addl. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)