proposition: Lemma half_gtnn n : (n./2 < n) = (n != 0).
proof: Proof. case: n => // [] [|n] //. rewrite eqn_leq [n.+2 <= _]leqNgt -[X in _ < X]odd_double_half -addnn addnA. by rewrite /= [~~ _ + _]addnS addSn !ltnS leq_addl. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)