proposition: Lemma uphalf_double_subn1 a : uphalf ((a.*2).-1) = a.
proof: Proof. case a. done. move => a'. simpl; by rewrite half_double. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)