proposition: Lemma Zpower_pos_pos: forall x e : positive, (0 < Zpower_pos (Zpos x) e)%Z.
proof: Proof. intros x e. rewrite Zpower_pos_nat. induction (nat_of_P e). exact (refl_equal Lt). change (Zpower_nat (Zpos x) (S n)) with ((Zpos x) * Zpower_nat (Zpos x) n)%Z. apply Zmult_lt_0_compat with (2 := IHn). exact (refl_equal Lt). Qed.
imports: Flocq.Core.Defs Gappa_common