@(transitive_le ? (∏_{p < S (2*n) | primeb p} (p\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
[@le_pi #p #ltp #primebp @le_exp
[@prime_to_lt_O @primeb_true_to_prime //
@(transitive_le ? (∏_{p < S (2*n) | primeb p} (p\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
[@le_pi #p #ltp #primebp @le_exp
[@prime_to_lt_O @primeb_true_to_prime //