fact: Fixpoint bertrand_fun_aux (n m : nat) {struct m} : nat := match primeb n with | true => n | false => match m with | O => 0 | S m1 => bertrand_fun_aux (S n) m1 end end.
imports: Coq(Div2 Even Wf_nat Arith ArithRing List) Bertrand(Bertrand)