proposition: Lemma div2_le n: div2 n <= n.
proof: Proof. suff: (div2 n <= n) /\ (div2 n.+1 <= n.+1) by case. elim: n=>//[n]. case: n=>// n; rewrite !div2orb; case=>H1 H2. split=>//. Search _ (_ < _.+1). rewrite -ltnS in H1. by move: (ltn_trans H1 (ltnSn n.+2)). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)