## Full example

    :: Example from http://webdocs.cs.ualberta.ca/~piotr/Mizar/Dagstuhl97/
    environ
    vocabulary SCM;
    constructors ARYTHM, PRE_FF, NAT_1, REAL_1;
    notation ARYTHM, PRE_FF, NAT_1;
    requirements ARYTHM;
    theorems REAL_1, PRE_FF, NAT_1, AXIOMS, CQC_THE1;
    schemes NAT_1;
    begin

    P: for k being Nat
    	st for n being Nat st n < k holds Fib (n+1) ≥ n
    		holds Fib (k+1) ≥ k
    proof let k be Nat; assume
    IH: for n being Nat st n < k holds Fib (n+1) ≥ n;
    	per cases;
    		suppose k ≤ 1; then k = 0 or k = 0+1 by CQC_THE1:2;
    			hence Fib (k+1) ≥ k by PRE_FF:1;
    		suppose 1 < k; then
    			1+1 ≤ k by NAT_1:38; then
    			consider m being Nat such that
    		A: k = 1+1+m by NAT_1:28;
    			thus Fib (k+1) ≥ k proof
    				per cases by NAT_1:19;
    				suppose S1: m = 0;
    					Fib (0+1+1+1) = Fib(0+1) + Fib(0+1+1) by PRE_FF:1
    					              = 1 + 1 by PRE_FF:1;
    					hence Fib (k+1) ≥ k by A, S1;
    				suppose m > 0; then
    					m+1 > 0+1 by REAL_1:59; then
    					m ≥ 1 by NAT_1:38; then
    				B: m+(m+1) ≥ m+1+1 by REAL_1:49;
    				C: k = m+1+1 by A, AXIOMS:13;
    				   m < m+1 & m+1 < m+1+1 by REAL_1:69; then
    				   m < k & m+1 < k by C, AXIOMS:22; then
    				D: Fib (m+1) ≥ m & Fib (m+1+1) ≥ m+1 by IH;
    				   Fib (m+1+1+1) = Fib (m+1) + Fib (m+1+1) by PRE_FF:1; then
    				   Fib (m+1+1+1) ≥ m+(m+1) by D, REAL_1:55;
    		hence Fib(k+1) ≥ k by C, B, AXIOMS:22;
    	end;
    end;

    for n being Nat holds Fib(n+1) ≥ n from Comp_Ind(P);