minFac

write a function that given a natural number a, a>1, find the minimum factor of a that is not 1. 

Function Signature

def minFac(a:Nat) (h: a>1): Nat 

Theorem Signature

theorem minFac_isfac(a:Nat)(h: a>1): ( (minFac a h) ∣a) ∧(minFac a h>1)

Additional Theorem Signature

theorem minFac_ismin(a:Nat)(h:a>1): Not (∃ y>1,( y ∣ a) ∧y<minFac a h)

View All Submissions

Please log in or register to submit a solution for this challenge.