proposition: Lemma half_sub a : forall b, a <= b.*2 -> (b.*2 - a)./2 = b - uphalf a.
proof: Proof. induction a => b H. + by rewrite !subn0 doubleK. + rewrite half_subn1. rewrite uphalf_half. rewrite IHa. rewrite oddB. rewrite odd_double/=. rewrite -subn1. rewrite uphalf_half. case ODD: (odd a). by rewrite add1n subn1. by rewrite !add0n/= -subnDA addn1. apply (ltnW H). apply (ltnW H). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)