let n be non zero square-free Nat; :: thesis: for a being non zero Nat st a divides n holds
a,n div a are_coprime
let a be non zero Nat; :: thesis: ( a divides n implies a,n div a are_coprime )
assume A0: a divides n ; :: thesis: a,n div a are_coprime
assume Z1: not a,n div a are_coprime ; :: thesis: contradiction
Z2: n div a <> 0

proof

assume n div a = 0 ; :: thesis: contradiction
then n < a by NAT_2:12;
hence contradiction by NAT_D:7, A0; :: thesis: verum

end;

consider k being non zero Nat such that
A1: ( k <> 1 & k divides a & k divides n div a ) by RelPrimeEx, Z1, Z2;
a * (n div a) = n by A0, NAT_D:3;
then k ^2 divides n by A1, NAT_3:1;
hence contradiction by A1, SqCon1; :: thesis: verum