environ

    == We interpret the predicates Div and Mult as follows:
    ==           Div[x,y,z] iff x / y = z
    ==           Mult[x,y,z] iff  x * y = z

reserve x,y,z,t,p for Real;

A1: for x,y,z holds Div[x, y, z] iff Mult[z, y, x];

A2: for x,y,z,t holds Div[z, t, x] & Div[z, t, y] implies x=y;

A3: ex p st for x holds Mult[x, p, p];

begin

absurd: for x, y holds x=y proof
    let x, y be Real;
           consider p such that
       B1: for t holds Mult[t, p, p] by A3;
        1: Mult[x, p, p] & Mult[y, p, p] by B1;
        2: Div[p, p, x] & Div[p, p, y] by 1, A1;
        3: x=y by 2, A2;
    thus thesis by 3;
end;