let k, l be Nat; :: thesis: ( l >= 1 implies k * l >= k )
assume A1: l >= 1 ; :: thesis: k * l >= k
for k being Nat holds k * l >= k

proof

defpred S₁[ Nat] means $1 * l >= $1;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A3: (k + 1) * l = (k * l) + (1 * l) ;
A4: k + l >= k + 1 by A1, XREAL_1:7;
assume k * l >= k ; :: thesis: S₁[k + 1]
then (k + 1) * l >= k + l by A3, XREAL_1:7;
hence (k + 1) * l >= k + 1 by A4, XXREAL_0:2; :: thesis: verum

end;

A5: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A2); :: thesis: verum

end;

hence k * l >= k ; :: thesis: verum