proposition: Lemma trunc_gt0 x : (0 < trunc x)%N = (1 <= x).
proof: Proof. case: ifP (truncP x) => [le0x /andP[lemx ltxm1] | le0x /eqP ->]; last first. by apply/esym; apply/contraFF/le_trans: le0x. apply/idP/idP => [m_gt0 | x_ge1]; first by apply: le_trans lemx; rewrite ler1n. by rewrite -ltnS -(ltr_nat R) (le_lt_trans x_ge1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)