proposition: Lemma all_rat_in_P_pos l: all rat_in_P l -> all (> 0) l.
proof: Proof. move => aa. apply/allP => i /(allP aa) / rat_in_P_ge1 h. exact: (Order.POrderTheory.lt_le_trans ltr01 h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)