proposition: Lemma p4_pos (n : int) : n >= 0 -> p4 n > 0.
proof: Proof. move=> h. apply: (finite_diff_pos p3_is_fdiff_of_p4 p4_0_pos); last done. move: n h => _ _ n h. apply: (finite_diff_pos p2_is_fdiff_of_p3 p3_0_pos); last done. move: n h => _ _ n h. apply: (finite_diff_pos p1_is_fdiff_of_p2 p2_0_pos); last done. move: n h => _ _ n h. apply: (finite_diff_pos p0_is_fdiff_of_p1 p1_0_pos); last done. move: n h => _ _ n h. by rewrite /p0 rat_of_ZEdef ltr0z /nat_of_P /Pmult_nat /=. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics rat_of_Z