per cases ( a = 0 or a > 0 ) ;

suppose a = 0 ; :: thesis: frac a = cfrac a

hence frac a = cfrac a by INT_1:45; :: thesis: verum

end;

suppose a > 0 ; :: thesis: frac a = cfrac a

then reconsider a = a as positive Real ;
reconsider b = director a as positive weightless Real ;
( b = 1 & frac a = frac |.a.| ) by TA1;
hence frac a = cfrac a ; :: thesis: verum

end;

end;