proposition: Lemma half_double_subn1 a : ((a.*2).-1)./2 = a.-1.
proof: Proof. case a. done. move => a'. simpl; apply uphalf_double. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)