proposition: Lemma trunc0Pn x : reflect (trunc x = 0%N) (~~ (1 <= x)).
proof: Proof. by rewrite -trunc_gt0 -eqn0Ngt; apply: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)