proposition: Lemma half_subn1 : forall a b, (b - a.+1)./2 = (uphalf (b - a)).-1.
proof: Proof. induction a. + case => //. move => b. by rewrite subn1. + move => b. specialize (IHa (b.-1)). rewrite -subn1 in IHa. by rewrite -!subnDA !add1n in IHa. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)