registration let p, q be Element of Nat_Lattice; identify p "\/" q with p lcm q;compatibilityproof thus p "\/" q = p lcm q; end; end;

registration let a be Element of G_Real, x be real number; identify -a with -x when a = x;compatibilityproof thus a = x implies -a = -x; end; end;