let m, n be Nat; :: thesis: ( 1 < m implies (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n) )
assume AS: 1 < m ; :: thesis: (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n)

per cases ( n = 0 or not n is zero ) ;

suppose n = 0 ; :: thesis: (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n)

hence (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n) by DefLio; :: thesis: verum

end;

suppose not n is zero ; :: thesis: (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n)

hence (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n) by TC1, AS; :: thesis: verum

end;

end;