#n #posn (cases (le_to_or_lt_eq … posn))
[#lt1n @mod_O_to_divides [@lt_O_smallest_factor //]
>smallest_factor_to_min // @eqb_true_to_eq @f_min_true
#n #posn (cases (le_to_or_lt_eq … posn))
[#lt1n @mod_O_to_divides [@lt_O_smallest_factor //]
>smallest_factor_to_min // @eqb_true_to_eq @f_min_true