proposition: Lemma expn_gt0 m n : (0 < m ^ n) = (0 < m) || (n == 0).
proof: Proof. by case: m => [|m]; elim: n => //= n IHn; rewrite expnS // addn_gt0 IHn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring