proposition: Lemma uphalf_leq m n : m <= n -> uphalf m <= uphalf n.
proof: Proof. move/subnK <-; rewrite !uphalf_half oddD halfD !addnA. by do 2 case: odd; apply: leq_addl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring