include('Axioms/nets_2.ax').
tff(tp_ty_2Erat_2Erat,type,( ty_2Erat_2Erat: del )).
tff(stp_ty_2Erat_2Erat,type,(tp__ty_2Erat_2Erat : $tType)).
tff(stp_inj_ty_2Erat_2Erat,type,(inj__ty_2Erat_2Erat : tp__ty_2Erat_2Erat > $i)).
tff(stp_surj_ty_2Erat_2Erat,type,(surj__ty_2Erat_2Erat : $i > tp__ty_2Erat_2Erat)).
tff(stp_inj_surj_ty_2Erat_2Erat,axiom,( ! [X:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(inj__ty_2Erat_2Erat(X)) = X))).
tff(stp_inj_mem_ty_2Erat_2Erat,axiom,( ! [X:tp__ty_2Erat_2Erat] : (mem(inj__ty_2Erat_2Erat(X),ty_2Erat_2Erat)))).
tff(stp_iso_mem_ty_2Erat_2Erat,axiom,( ! [X:$i] : (mem(X,ty_2Erat_2Erat) => (X = inj__ty_2Erat_2Erat(surj__ty_2Erat_2Erat(X)))))).
tff(tp_c_2Erat_2ERATD,type,(c_2Erat_2ERATD:$i)).
tff(mem_c_2Erat_2ERATD,axiom,mem(c_2Erat_2ERATD,arr(ty_2Erat_2Erat,ty_2Enum_2Enum))).
tff(stp_fo_c_2Erat_2ERATD,type,(fo__c_2Erat_2ERATD:(tp__ty_2Erat_2Erat) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Erat_2ERATD,axiom,( ! [X0:tp__ty_2Erat_2Erat] : (inj__ty_2Enum_2Enum(fo__c_2Erat_2ERATD(X0)) = ap(c_2Erat_2ERATD,inj__ty_2Erat_2Erat(X0))))).
tff(tp_c_2Erat_2ERATN,type,(c_2Erat_2ERATN:$i)).
tff(mem_c_2Erat_2ERATN,axiom,mem(c_2Erat_2ERATN,arr(ty_2Erat_2Erat,ty_2Einteger_2Eint))).
tff(stp_fo_c_2Erat_2ERATN,type,(fo__c_2Erat_2ERATN:(tp__ty_2Erat_2Erat) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Erat_2ERATN,axiom,( ! [X0:tp__ty_2Erat_2Erat] : (inj__ty_2Einteger_2Eint(fo__c_2Erat_2ERATN(X0)) = ap(c_2Erat_2ERATN,inj__ty_2Erat_2Erat(X0))))).
tff(tp_c_2Erat_2Eabs__rat,type,(c_2Erat_2Eabs__rat:$i)).
tff(mem_c_2Erat_2Eabs__rat,axiom,mem(c_2Erat_2Eabs__rat,arr(ty_2Efrac_2Efrac,ty_2Erat_2Erat))).
tff(stp_fo_c_2Erat_2Eabs__rat,type,(fo__c_2Erat_2Eabs__rat:(tp__ty_2Efrac_2Efrac) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Eabs__rat,axiom,( ! [X0:tp__ty_2Efrac_2Efrac] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Eabs__rat(X0)) = ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(X0))))).
tff(tp_c_2Erat_2Eabs__rat__CLASS,type,(c_2Erat_2Eabs__rat__CLASS:$i)).
tff(mem_c_2Erat_2Eabs__rat__CLASS,axiom,mem(c_2Erat_2Eabs__rat__CLASS,arr(arr(ty_2Efrac_2Efrac,bool),ty_2Erat_2Erat))).
tff(tp_c_2Erat_2Erat__0,type,(c_2Erat_2Erat__0:$i)).
tff(mem_c_2Erat_2Erat__0,axiom,mem(c_2Erat_2Erat__0,ty_2Erat_2Erat)).
tff(stp_fo_c_2Erat_2Erat__0,type,(fo__c_2Erat_2Erat__0:tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__0,axiom,(inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__0) = c_2Erat_2Erat__0)).
tff(tp_c_2Erat_2Erat__1,type,(c_2Erat_2Erat__1:$i)).
tff(mem_c_2Erat_2Erat__1,axiom,mem(c_2Erat_2Erat__1,ty_2Erat_2Erat)).
tff(stp_fo_c_2Erat_2Erat__1,type,(fo__c_2Erat_2Erat__1:tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__1,axiom,(inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__1) = c_2Erat_2Erat__1)).
tff(tp_c_2Erat_2Erat__add,type,(c_2Erat_2Erat__add:$i)).
tff(mem_c_2Erat_2Erat__add,axiom,mem(c_2Erat_2Erat__add,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat)))).
tff(stp_fo_c_2Erat_2Erat__add,type,(fo__c_2Erat_2Erat__add:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__add,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__add(X0,X1)) = ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erat__ainv,type,(c_2Erat_2Erat__ainv:$i)).
tff(mem_c_2Erat_2Erat__ainv,axiom,mem(c_2Erat_2Erat__ainv,arr(ty_2Erat_2Erat,ty_2Erat_2Erat))).
tff(stp_fo_c_2Erat_2Erat__ainv,type,(fo__c_2Erat_2Erat__ainv:(tp__ty_2Erat_2Erat) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__ainv,axiom,( ! [X0:tp__ty_2Erat_2Erat] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__ainv(X0)) = ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(X0))))).
tff(tp_c_2Erat_2Erat__cons,type,(c_2Erat_2Erat__cons:$i)).
tff(mem_c_2Erat_2Erat__cons,axiom,mem(c_2Erat_2Erat__cons,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Erat_2Erat)))).
tff(stp_fo_c_2Erat_2Erat__cons,type,(fo__c_2Erat_2Erat__cons:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__cons,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__cons(X0,X1)) = ap(ap(c_2Erat_2Erat__cons,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Erat_2Erat__div,type,(c_2Erat_2Erat__div:$i)).
tff(mem_c_2Erat_2Erat__div,axiom,mem(c_2Erat_2Erat__div,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat)))).
tff(stp_fo_c_2Erat_2Erat__div,type,(fo__c_2Erat_2Erat__div:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__div,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__div(X0,X1)) = ap(ap(c_2Erat_2Erat__div,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erat__dnm,type,(c_2Erat_2Erat__dnm:$i)).
tff(mem_c_2Erat_2Erat__dnm,axiom,mem(c_2Erat_2Erat__dnm,arr(ty_2Erat_2Erat,ty_2Einteger_2Eint))).
tff(stp_fo_c_2Erat_2Erat__dnm,type,(fo__c_2Erat_2Erat__dnm:(tp__ty_2Erat_2Erat) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Erat_2Erat__dnm,axiom,( ! [X0:tp__ty_2Erat_2Erat] : (inj__ty_2Einteger_2Eint(fo__c_2Erat_2Erat__dnm(X0)) = ap(c_2Erat_2Erat__dnm,inj__ty_2Erat_2Erat(X0))))).
tff(tp_c_2Erat_2Erat__equiv,type,(c_2Erat_2Erat__equiv:$i)).
tff(mem_c_2Erat_2Erat__equiv,axiom,mem(c_2Erat_2Erat__equiv,arr(ty_2Efrac_2Efrac,arr(ty_2Efrac_2Efrac,bool)))).
tff(stp_fo_c_2Erat_2Erat__equiv,type,(fo__c_2Erat_2Erat__equiv:(tp__ty_2Efrac_2Efrac * tp__ty_2Efrac_2Efrac) > tp__o)).
tff(stp_eq_fo_c_2Erat_2Erat__equiv,axiom,( ! [X0:tp__ty_2Efrac_2Efrac] : ( ! [X1:tp__ty_2Efrac_2Efrac] : (inj__o(fo__c_2Erat_2Erat__equiv(X0,X1)) = ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(X0)),inj__ty_2Efrac_2Efrac(X1)))))).
tff(tp_c_2Erat_2Erat__geq,type,(c_2Erat_2Erat__geq:$i)).
tff(mem_c_2Erat_2Erat__geq,axiom,mem(c_2Erat_2Erat__geq,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,bool)))).
tff(stp_fo_c_2Erat_2Erat__geq,type,(fo__c_2Erat_2Erat__geq:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__o)).
tff(stp_eq_fo_c_2Erat_2Erat__geq,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__o(fo__c_2Erat_2Erat__geq(X0,X1)) = ap(ap(c_2Erat_2Erat__geq,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erat__gre,type,(c_2Erat_2Erat__gre:$i)).
tff(mem_c_2Erat_2Erat__gre,axiom,mem(c_2Erat_2Erat__gre,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,bool)))).
tff(stp_fo_c_2Erat_2Erat__gre,type,(fo__c_2Erat_2Erat__gre:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__o)).
tff(stp_eq_fo_c_2Erat_2Erat__gre,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__o(fo__c_2Erat_2Erat__gre(X0,X1)) = ap(ap(c_2Erat_2Erat__gre,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erat__leq,type,(c_2Erat_2Erat__leq:$i)).
tff(mem_c_2Erat_2Erat__leq,axiom,mem(c_2Erat_2Erat__leq,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,bool)))).
tff(stp_fo_c_2Erat_2Erat__leq,type,(fo__c_2Erat_2Erat__leq:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__o)).
tff(stp_eq_fo_c_2Erat_2Erat__leq,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__o(fo__c_2Erat_2Erat__leq(X0,X1)) = ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erat__les,type,(c_2Erat_2Erat__les:$i)).
tff(mem_c_2Erat_2Erat__les,axiom,mem(c_2Erat_2Erat__les,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,bool)))).
tff(stp_fo_c_2Erat_2Erat__les,type,(fo__c_2Erat_2Erat__les:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__o)).
tff(stp_eq_fo_c_2Erat_2Erat__les,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__o(fo__c_2Erat_2Erat__les(X0,X1)) = ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erat__max,type,(c_2Erat_2Erat__max:$i)).
tff(mem_c_2Erat_2Erat__max,axiom,mem(c_2Erat_2Erat__max,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat)))).
tff(stp_fo_c_2Erat_2Erat__max,type,(fo__c_2Erat_2Erat__max:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__max,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__max(X0,X1)) = ap(ap(c_2Erat_2Erat__max,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erat__min,type,(c_2Erat_2Erat__min:$i)).
tff(mem_c_2Erat_2Erat__min,axiom,mem(c_2Erat_2Erat__min,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat)))).
tff(stp_fo_c_2Erat_2Erat__min,type,(fo__c_2Erat_2Erat__min:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__min,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__min(X0,X1)) = ap(ap(c_2Erat_2Erat__min,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erat__minv,type,(c_2Erat_2Erat__minv:$i)).
tff(mem_c_2Erat_2Erat__minv,axiom,mem(c_2Erat_2Erat__minv,arr(ty_2Erat_2Erat,ty_2Erat_2Erat))).
tff(stp_fo_c_2Erat_2Erat__minv,type,(fo__c_2Erat_2Erat__minv:(tp__ty_2Erat_2Erat) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__minv,axiom,( ! [X0:tp__ty_2Erat_2Erat] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__minv(X0)) = ap(c_2Erat_2Erat__minv,inj__ty_2Erat_2Erat(X0))))).
tff(tp_c_2Erat_2Erat__mul,type,(c_2Erat_2Erat__mul:$i)).
tff(mem_c_2Erat_2Erat__mul,axiom,mem(c_2Erat_2Erat__mul,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat)))).
tff(stp_fo_c_2Erat_2Erat__mul,type,(fo__c_2Erat_2Erat__mul:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__mul,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__mul(X0,X1)) = ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erat__nmr,type,(c_2Erat_2Erat__nmr:$i)).
tff(mem_c_2Erat_2Erat__nmr,axiom,mem(c_2Erat_2Erat__nmr,arr(ty_2Erat_2Erat,ty_2Einteger_2Eint))).
tff(stp_fo_c_2Erat_2Erat__nmr,type,(fo__c_2Erat_2Erat__nmr:(tp__ty_2Erat_2Erat) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Erat_2Erat__nmr,axiom,( ! [X0:tp__ty_2Erat_2Erat] : (inj__ty_2Einteger_2Eint(fo__c_2Erat_2Erat__nmr(X0)) = ap(c_2Erat_2Erat__nmr,inj__ty_2Erat_2Erat(X0))))).
tff(tp_c_2Erat_2Erat__of__int,type,(c_2Erat_2Erat__of__int:$i)).
tff(mem_c_2Erat_2Erat__of__int,axiom,mem(c_2Erat_2Erat__of__int,arr(ty_2Einteger_2Eint,ty_2Erat_2Erat))).
tff(stp_fo_c_2Erat_2Erat__of__int,type,(fo__c_2Erat_2Erat__of__int:(tp__ty_2Einteger_2Eint) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__of__int,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__of__int(X0)) = ap(c_2Erat_2Erat__of__int,inj__ty_2Einteger_2Eint(X0))))).
tff(tp_c_2Erat_2Erat__of__num,type,(c_2Erat_2Erat__of__num:$i)).
tff(mem_c_2Erat_2Erat__of__num,axiom,mem(c_2Erat_2Erat__of__num,arr(ty_2Enum_2Enum,ty_2Erat_2Erat))).
tff(stp_fo_c_2Erat_2Erat__of__num,type,(fo__c_2Erat_2Erat__of__num:(tp__ty_2Enum_2Enum) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__of__num,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__of__num(X0)) = ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Erat_2Erat__sgn,type,(c_2Erat_2Erat__sgn:$i)).
tff(mem_c_2Erat_2Erat__sgn,axiom,mem(c_2Erat_2Erat__sgn,arr(ty_2Erat_2Erat,ty_2Einteger_2Eint))).
tff(stp_fo_c_2Erat_2Erat__sgn,type,(fo__c_2Erat_2Erat__sgn:(tp__ty_2Erat_2Erat) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Erat_2Erat__sgn,axiom,( ! [X0:tp__ty_2Erat_2Erat] : (inj__ty_2Einteger_2Eint(fo__c_2Erat_2Erat__sgn(X0)) = ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(X0))))).
tff(tp_c_2Erat_2Erat__sub,type,(c_2Erat_2Erat__sub:$i)).
tff(mem_c_2Erat_2Erat__sub,axiom,mem(c_2Erat_2Erat__sub,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat)))).
tff(stp_fo_c_2Erat_2Erat__sub,type,(fo__c_2Erat_2Erat__sub:(tp__ty_2Erat_2Erat * tp__ty_2Erat_2Erat) > tp__ty_2Erat_2Erat)).
tff(stp_eq_fo_c_2Erat_2Erat__sub,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : (inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__sub(X0,X1)) = ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(X0)),inj__ty_2Erat_2Erat(X1)))))).
tff(tp_c_2Erat_2Erep__rat,type,(c_2Erat_2Erep__rat:$i)).
tff(mem_c_2Erat_2Erep__rat,axiom,mem(c_2Erat_2Erep__rat,arr(ty_2Erat_2Erat,ty_2Efrac_2Efrac))).
tff(stp_fo_c_2Erat_2Erep__rat,type,(fo__c_2Erat_2Erep__rat:(tp__ty_2Erat_2Erat) > tp__ty_2Efrac_2Efrac)).
tff(stp_eq_fo_c_2Erat_2Erep__rat,axiom,( ! [X0:tp__ty_2Erat_2Erat] : (inj__ty_2Efrac_2Efrac(fo__c_2Erat_2Erep__rat(X0)) = ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(X0))))).
tff(tp_c_2Erat_2Erep__rat__CLASS,type,(c_2Erat_2Erep__rat__CLASS:$i)).
tff(mem_c_2Erat_2Erep__rat__CLASS,axiom,mem(c_2Erat_2Erep__rat__CLASS,arr(ty_2Erat_2Erat,arr(ty_2Efrac_2Efrac,bool)))).
tff(stp_fo_c_2Erat_2Erep__rat__CLASS,type,(fo__c_2Erat_2Erep__rat__CLASS:(tp__ty_2Erat_2Erat * tp__ty_2Efrac_2Efrac) > tp__o)).
tff(stp_eq_fo_c_2Erat_2Erep__rat__CLASS,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Efrac_2Efrac] : (inj__o(fo__c_2Erat_2Erep__rat__CLASS(X0,X1)) = ap(ap(c_2Erat_2Erep__rat__CLASS,inj__ty_2Erat_2Erat(X0)),inj__ty_2Efrac_2Efrac(X1)))))).
tff(ax_thm_2Erat_2Erat__equiv__def,axiom,( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0f1)),inj__ty_2Efrac_2Efrac(V1f2))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V1f2)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1f2))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V0f1))))))))).
tff(conj_thm_2Erat_2ERAT__EQUIV__REF,lemma,(( ! [V0a:tp__ty_2Efrac_2Efrac] : p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0a)),inj__ty_2Efrac_2Efrac(V0a)))))).
tff(conj_thm_2Erat_2ERAT__EQUIV__SYM,lemma,(( ! [V0a:tp__ty_2Efrac_2Efrac] : ( ! [V1b:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0a)),inj__ty_2Efrac_2Efrac(V1b))) <=> p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V1b)),inj__ty_2Efrac_2Efrac(V0a)))))))).
tff(conj_thm_2Erat_2ERAT__EQUIV__NMR__Z__IFF,lemma,(( ! [V0a:tp__ty_2Efrac_2Efrac] : ( ! [V1b:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0a)),inj__ty_2Efrac_2Efrac(V1b))) => ((surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0a))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1b))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Erat_2ERAT__EQUIV__NMR__GTZ__IFF,lemma,(( ! [V0a:tp__ty_2Efrac_2Efrac] : ( ! [V1b:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0a)),inj__ty_2Efrac_2Efrac(V1b))) => (p(ap(ap(c_2Einteger_2Eint__gt,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0a))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__gt,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1b))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Erat_2ERAT__EQUIV__NMR__LTZ__IFF,lemma,(( ! [V0a:tp__ty_2Efrac_2Efrac] : ( ! [V1b:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0a)),inj__ty_2Efrac_2Efrac(V1b))) => (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0a))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1b))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Erat_2ERAT__NMR__Z__IFF__EQUIV,lemma,(( ! [V0a:tp__ty_2Efrac_2Efrac] : ( ! [V1b:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0a))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) => (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0a)),inj__ty_2Efrac_2Efrac(V1b))) <=> (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1b))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Erat_2ERAT__EQUIV__TRANS,lemma,(( ! [V0a:tp__ty_2Efrac_2Efrac] : ( ! [V1b:tp__ty_2Efrac_2Efrac] : ( ! [V2c:tp__ty_2Efrac_2Efrac] : ((p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0a)),inj__ty_2Efrac_2Efrac(V1b))) & p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V1b)),inj__ty_2Efrac_2Efrac(V2c)))) => p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0a)),inj__ty_2Efrac_2Efrac(V2c))))))))).
tff(conj_thm_2Erat_2ERAT__EQUIV,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0f1)),inj__ty_2Efrac_2Efrac(V1f2))) <=> (ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0f1)) = ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V1f2)))))))).
tff(conj_thm_2Erat_2ERAT__EQUIV__ALT,lemma,(( ! [V0a:tp__ty_2Efrac_2Efrac] : (ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0a)) = f2853(V0a))))).
tff(ax_thm_2Erat_2Erat__TY__DEF,axiom,(? [V0rep:$i] : (mem(V0rep,arr(ty_2Erat_2Erat,arr(ty_2Efrac_2Efrac,bool))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(arr(ty_2Efrac_2Efrac,bool),ty_2Erat_2Erat),f2855),V0rep))))).
tff(ax_thm_2Erat_2Erat__bijections,axiom,(( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat__CLASS,ap(c_2Erat_2Erep__rat__CLASS,inj__ty_2Erat_2Erat(V0a)))) = V0a)) & ( ! [V1r:$i] : (mem(V1r,arr(ty_2Efrac_2Efrac,bool)) => (p(ap(f2857,V1r)) <=> (ap(c_2Erat_2Erep__rat__CLASS,ap(c_2Erat_2Eabs__rat__CLASS,V1r)) = V1r)))))).
tff(conj_thm_2Erat_2Erat__ABS__REP__CLASS,lemma,((( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat__CLASS,ap(c_2Erat_2Erep__rat__CLASS,inj__ty_2Erat_2Erat(V0a)))) = V0a)) & ( ! [V1c:$i] : (mem(V1c,arr(ty_2Efrac_2Efrac,bool)) => ((? [V2r:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V2r)),inj__ty_2Efrac_2Efrac(V2r))) & (V1c = ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V2r))))) <=> (ap(c_2Erat_2Erep__rat__CLASS,ap(c_2Erat_2Eabs__rat__CLASS,V1c)) = V1c))))))).
tff(ax_thm_2Erat_2Erep__rat__def,axiom,( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Efrac_2Efrac(ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0a))) = surj__ty_2Efrac_2Efrac(ap(c_2Emin_2E_40(ty_2Efrac_2Efrac),ap(c_2Erat_2Erep__rat__CLASS,inj__ty_2Erat_2Erat(V0a))))))).
tff(ax_thm_2Erat_2Eabs__rat__def,axiom,( ! [V0r:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0r))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat__CLASS,ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0r))))))).
tff(conj_thm_2Erat_2Erat__QUOTIENT,lemma,(p(ap(ap(ap(c_2Equotient_2EQUOTIENT(ty_2Efrac_2Efrac,ty_2Erat_2Erat),c_2Erat_2Erat__equiv),c_2Erat_2Eabs__rat),c_2Erat_2Erep__rat)))).
tff(conj_thm_2Erat_2Erat__def,lemma,(p(ap(ap(ap(c_2Equotient_2EQUOTIENT(ty_2Efrac_2Efrac,ty_2Erat_2Erat),c_2Erat_2Erat__equiv),c_2Erat_2Eabs__rat),c_2Erat_2Erep__rat)))).
tff(conj_thm_2Erat_2Erat__type__thm,lemma,((( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0a)))) = V0a)) & ( ! [V1r:tp__ty_2Efrac_2Efrac] : ( ! [V2s:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V1r)),inj__ty_2Efrac_2Efrac(V2s))) <=> (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1r))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V2s)))))))))).
tff(conj_thm_2Erat_2Erat__equiv__reps,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__equiv,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V1r2)))) <=> (V0r1 = V1r2)))))).
tff(conj_thm_2Erat_2Erat__equiv__rep__abs,lemma,(( ! [V0f:tp__ty_2Efrac_2Efrac] : p(ap(ap(c_2Erat_2Erat__equiv,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f)))),inj__ty_2Efrac_2Efrac(V0f)))))).
tff(ax_thm_2Erat_2Erat__nmr__def,axiom,( ! [V0r:tp__ty_2Erat_2Erat] : (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__nmr,inj__ty_2Erat_2Erat(V0r))) = surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r))))))).
tff(ax_thm_2Erat_2Erat__dnm__def,axiom,( ! [V0r:tp__ty_2Erat_2Erat] : (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__dnm,inj__ty_2Erat_2Erat(V0r))) = surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__dnm,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r))))))).
tff(ax_thm_2Erat_2Erat__sgn__def,axiom,( ! [V0r:tp__ty_2Erat_2Erat] : (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r))) = surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__sgn,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r))))))).
tff(ax_thm_2Erat_2Erat__0__def,axiom,(fo__c_2Erat_2Erat__0 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(fo__c_2Efrac_2Efrac__0))))).
tff(ax_thm_2Erat_2Erat__1__def,axiom,(fo__c_2Erat_2Erat__1 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(fo__c_2Efrac_2Efrac__1))))).
tff(ax_thm_2Erat_2Erat__ainv__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__ainv,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r1)))))))).
tff(ax_thm_2Erat_2Erat__minv__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__minv,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__minv,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r1)))))))).
tff(ax_thm_2Erat_2Erat__add__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(ax_thm_2Erat_2Erat__sub__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(ax_thm_2Erat_2Erat__mul__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(ax_thm_2Erat_2Erat__div__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__div,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(ax_thm_2Erat_2Erat__les__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) <=> (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(ax_thm_2Erat_2Erat__gre__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__gre,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) <=> p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1))))))).
tff(ax_thm_2Erat_2Erat__leq__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) <=> (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) | (V0r1 = V1r2)))))).
tff(ax_thm_2Erat_2Erat__geq__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__geq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) <=> p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1))))))).
tff(ax_thm_2Erat_2Erat__cons__def,axiom,( ! [V0nmr:tp__ty_2Einteger_2Eint] : ( ! [V1dnm:tp__ty_2Einteger_2Eint] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__cons,inj__ty_2Einteger_2Eint(V0nmr)),inj__ty_2Einteger_2Eint(V1dnm))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Eabs__frac,ap(ap(c_2Epair_2E_2C(ty_2Einteger_2Eint,ty_2Einteger_2Eint),ap(ap(c_2Einteger_2Eint__mul,ap(ap(c_2Einteger_2Eint__mul,ap(c_2EintExtension_2ESGN,inj__ty_2Einteger_2Eint(V0nmr))),ap(c_2EintExtension_2ESGN,inj__ty_2Einteger_2Eint(V1dnm)))),ap(c_2Einteger_2EABS,inj__ty_2Einteger_2Eint(V0nmr)))),ap(c_2Einteger_2EABS,inj__ty_2Einteger_2Eint(V1dnm)))))))))).
tff(ax_thm_2Erat_2Erat__of__num__primitive__def,axiom,(c_2Erat_2Erat__of__num = ap(ap(c_2Erelation_2EWFREC(ty_2Enum_2Enum,ty_2Erat_2Erat),ap(c_2Emin_2E_40(arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),f2859)),f2863))).
tff(conj_thm_2Erat_2Erat__of__num__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ((p(ap(V0P,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) & (p(ap(V0P,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(V0P,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) => p(ap(V0P,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))))))))) => ( ! [V2v:tp__ty_2Enum_2Enum] : p(ap(V0P,inj__ty_2Enum_2Enum(V2v))))))))).
tff(conj_thm_2Erat_2Erat__of__num__def,lemma,(((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Erat_2Erat__0) & ((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = fo__c_2Erat_2Erat__1) & ( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))),inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__1))))))))).
tff(conj_thm_2Erat_2Erat__of__num__def__compute,lemma,(((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Erat_2Erat__0) & ((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = fo__c_2Erat_2Erat__1) & (( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))))),inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__1))))) & ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1n)))))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1n))))),inj__ty_2Erat_2Erat(fo__c_2Erat_2Erat__1)))))))))).
tff(conj_thm_2Erat_2Erat__0,lemma,((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(fo__c_2Efrac_2Efrac__0)))))).
tff(conj_thm_2Erat_2Erat__1,lemma,((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(fo__c_2Efrac_2Efrac__1)))))).
tff(conj_thm_2Erat_2ERAT,lemma,(( ! [V0r:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Erat_2Erep__rat,inj__ty_2Erat_2Erat(V0r)))) = V0r)))).
tff(conj_thm_2Erat_2ERAT__ABS__EQUIV,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1f2)))) <=> p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0f1)),inj__ty_2Efrac_2Efrac(V1f2)))))))).
tff(conj_thm_2Erat_2ERAT__EQ,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1f2)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V1f2)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1f2))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V0f1)))))))))).
tff(conj_thm_2Erat_2ERAT__EQ__ALT,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((V0r1 = V1r2) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Erat_2Erat__nmr,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Erat_2Erat__dnm,inj__ty_2Erat_2Erat(V1r2)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Erat_2Erat__nmr,inj__ty_2Erat_2Erat(V1r2))),ap(c_2Erat_2Erat__dnm,inj__ty_2Erat_2Erat(V0r1)))))))))).
tff(conj_thm_2Erat_2ERAT__NMREQ0__CONG,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Erat_2ERAT__NMRLT0__CONG,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Efrac_2Efrac__nmr,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Erat_2ERAT__NMRGT0__CONG,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Einteger_2Eint__gt,ap(c_2Efrac_2Efrac__nmr,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__gt,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Erat_2ERAT__SGN__CONG,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__sgn,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))))) = surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__sgn,inj__ty_2Efrac_2Efrac(V0f1))))))).
tff(conj_thm_2Erat_2ERAT__AINV__CONG,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__ainv,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__ainv,inj__ty_2Efrac_2Efrac(V0x)))))))).
tff(conj_thm_2Erat_2EFRAC__MINV__EQUIV,lemma,(( ! [V0y:tp__ty_2Efrac_2Efrac] : ( ! [V1x:tp__ty_2Efrac_2Efrac] : ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V1x)),inj__ty_2Efrac_2Efrac(V0y))) => p(ap(ap(c_2Erat_2Erat__equiv,ap(c_2Efrac_2Efrac__minv,inj__ty_2Efrac_2Efrac(V1x))),ap(c_2Efrac_2Efrac__minv,inj__ty_2Efrac_2Efrac(V0y)))))))))).
tff(conj_thm_2Erat_2ERAT__MINV__CONG,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__minv,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__minv,inj__ty_2Efrac_2Efrac(V0x))))))))).
tff(conj_thm_2Erat_2EFRAC__ADD__EQUIV1,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1x_27:tp__ty_2Efrac_2Efrac] : ( ! [V2y:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1x_27))) => p(ap(ap(c_2Erat_2Erat__equiv,ap(ap(c_2Efrac_2Efrac__add,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V2y))),ap(ap(c_2Efrac_2Efrac__add,inj__ty_2Efrac_2Efrac(V1x_27)),inj__ty_2Efrac_2Efrac(V2y)))))))))).
tff(conj_thm_2Erat_2ERAT__ADD__CONG1,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))),inj__ty_2Efrac_2Efrac(V1y)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y))))))))).
tff(conj_thm_2Erat_2ERAT__ADD__CONG2,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,inj__ty_2Efrac_2Efrac(V0x)),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1y)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y))))))))).
tff(conj_thm_2Erat_2ERAT__ADD__CONG,lemma,((( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))),inj__ty_2Efrac_2Efrac(V1y)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y))))))) & ( ! [V2x:tp__ty_2Efrac_2Efrac] : ( ! [V3y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,inj__ty_2Efrac_2Efrac(V2x)),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V3y)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,inj__ty_2Efrac_2Efrac(V2x)),inj__ty_2Efrac_2Efrac(V3y)))))))))).
tff(conj_thm_2Erat_2EFRAC__MUL__EQUIV1,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1x_27:tp__ty_2Efrac_2Efrac] : ( ! [V2y:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1x_27))) => p(ap(ap(c_2Erat_2Erat__equiv,ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V2y))),ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V1x_27)),inj__ty_2Efrac_2Efrac(V2y)))))))))).
tff(conj_thm_2Erat_2EFRAC__MUL__EQUIV2,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1x_27:tp__ty_2Efrac_2Efrac] : ( ! [V2y:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__equiv,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1x_27))) => p(ap(ap(c_2Erat_2Erat__equiv,ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V2y)),inj__ty_2Efrac_2Efrac(V0x))),ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V2y)),inj__ty_2Efrac_2Efrac(V1x_27)))))))))).
tff(conj_thm_2Erat_2ERAT__MUL__CONG1,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))),inj__ty_2Efrac_2Efrac(V1y)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y))))))))).
tff(conj_thm_2Erat_2ERAT__MUL__CONG2,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V0x)),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1y)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y))))))))).
tff(conj_thm_2Erat_2ERAT__MUL__CONG,lemma,((( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))),inj__ty_2Efrac_2Efrac(V1y)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y))))))) & ( ! [V2x:tp__ty_2Efrac_2Efrac] : ( ! [V3y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V2x)),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V3y)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V2x)),inj__ty_2Efrac_2Efrac(V3y)))))))))).
tff(conj_thm_2Erat_2ERAT__SUB__CONG1,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))),inj__ty_2Efrac_2Efrac(V1y)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y))))))))).
tff(conj_thm_2Erat_2ERAT__SUB__CONG2,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,inj__ty_2Efrac_2Efrac(V0x)),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1y)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y))))))))).
tff(conj_thm_2Erat_2ERAT__SUB__CONG,lemma,((( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))),inj__ty_2Efrac_2Efrac(V1y)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y))))))) & ( ! [V2x:tp__ty_2Efrac_2Efrac] : ( ! [V3y:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,inj__ty_2Efrac_2Efrac(V2x)),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V3y)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,inj__ty_2Efrac_2Efrac(V2x)),inj__ty_2Efrac_2Efrac(V3y)))))))))).
tff(conj_thm_2Erat_2ERAT__DIV__CONG1,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))),inj__ty_2Efrac_2Efrac(V1y)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y)))))))))).
tff(conj_thm_2Erat_2ERAT__DIV__CONG2,lemma,(( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,inj__ty_2Efrac_2Efrac(V0x)),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1y)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y)))))))))).
tff(conj_thm_2Erat_2ERAT__DIV__CONG,lemma,((( ! [V0x:tp__ty_2Efrac_2Efrac] : ( ! [V1y:tp__ty_2Efrac_2Efrac] : ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0x)))),inj__ty_2Efrac_2Efrac(V1y)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,inj__ty_2Efrac_2Efrac(V0x)),inj__ty_2Efrac_2Efrac(V1y)))))))) & ( ! [V2x:tp__ty_2Efrac_2Efrac] : ( ! [V3y:tp__ty_2Efrac_2Efrac] : ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V3y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,inj__ty_2Efrac_2Efrac(V2x)),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V3y)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,inj__ty_2Efrac_2Efrac(V2x)),inj__ty_2Efrac_2Efrac(V3y))))))))))).
tff(conj_thm_2Erat_2ERAT__NMRDNM__EQ,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Eabs__frac,ap(ap(c_2Epair_2E_2C(ty_2Einteger_2Eint,ty_2Einteger_2Eint),ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V0f1)))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))) = surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V0f1)))))))).
tff(conj_thm_2Erat_2ERAT__AINV__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__ainv,inj__ty_2Efrac_2Efrac(V0f1)))))))).
tff(conj_thm_2Erat_2ERAT__MINV__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))))) => (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__minv,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__minv,inj__ty_2Efrac_2Efrac(V0f1))))))))).
tff(conj_thm_2Erat_2ERAT__ADD__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1f2)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,inj__ty_2Efrac_2Efrac(V0f1)),inj__ty_2Efrac_2Efrac(V1f2))))))))).
tff(conj_thm_2Erat_2ERAT__SUB__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1f2)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,inj__ty_2Efrac_2Efrac(V0f1)),inj__ty_2Efrac_2Efrac(V1f2))))))))).
tff(conj_thm_2Erat_2ERAT__MUL__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1f2)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,inj__ty_2Efrac_2Efrac(V0f1)),inj__ty_2Efrac_2Efrac(V1f2))))))))).
tff(conj_thm_2Erat_2ERAT__DIV__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1f2))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__div,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1f2)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,inj__ty_2Efrac_2Efrac(V0f1)),inj__ty_2Efrac_2Efrac(V1f2)))))))))).
tff(conj_thm_2Erat_2ERAT__EQ__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1f2)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V1f2)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1f2))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V0f1)))))))))).
tff(conj_thm_2Erat_2ERAT__LES__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1f2)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V1f2)))),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1f2))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V0f1)))))))))).
tff(conj_thm_2Erat_2ERAT__LEQ__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : (p(ap(ap(c_2Erat_2Erat__leq,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V1f2)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V0f1))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V1f2)))),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,inj__ty_2Efrac_2Efrac(V1f2))),ap(c_2Efrac_2Efrac__dnm,inj__ty_2Efrac_2Efrac(V0f1)))))))))).
tff(conj_thm_2Erat_2ERAT__OF__NUM__CALCULATE,lemma,(( ! [V0n1:tp__ty_2Enum_2Enum] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(V0n1))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Eabs__frac,ap(ap(c_2Epair_2E_2C(ty_2Einteger_2Eint,ty_2Einteger_2Eint),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n1))),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Erat_2ERAT__OF__NUM__LEQ,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Erat_2Erat__leq,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(V0a))),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(V1b)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b)))))))).
tff(conj_thm_2Erat_2ERAT__OF__NUM__LES,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(V0a))),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(V1b)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b)))))))).
tff(conj_thm_2Erat_2ERAT__EQ0__NMR,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ((V0r1 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__nmr,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Erat_2ERAT__0LES__NMR,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V0r1))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Erat_2Erat__nmr,inj__ty_2Erat_2Erat(V0r1)))))))).
tff(conj_thm_2Erat_2ERAT__LES0__NMR,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Erat_2Erat__nmr,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Erat_2ERAT__0LEQ__NMR,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__leq,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V0r1))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Erat_2Erat__nmr,inj__ty_2Erat_2Erat(V0r1)))))))).
tff(conj_thm_2Erat_2ERAT__LEQ0__NMR,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Erat_2Erat__nmr,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Erat_2ERAT__ADD__ASSOC,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0a)),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V1b)),inj__ty_2Erat_2Erat(V2c)))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b))),inj__ty_2Erat_2Erat(V2c))))))))).
tff(conj_thm_2Erat_2ERAT__MUL__ASSOC,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0a)),ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V1b)),inj__ty_2Erat_2Erat(V2c)))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b))),inj__ty_2Erat_2Erat(V2c))))))))).
tff(conj_thm_2Erat_2ERAT__ADD__COMM,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V1b)),inj__ty_2Erat_2Erat(V0a)))))))).
tff(conj_thm_2Erat_2ERAT__MUL__COMM,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V1b)),inj__ty_2Erat_2Erat(V0a)))))))).
tff(conj_thm_2Erat_2ERAT__ADD__RID,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0a)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0a)))).
tff(conj_thm_2Erat_2ERAT__ADD__LID,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V0a))) = V0a)))).
tff(conj_thm_2Erat_2ERAT__MUL__RID,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0a)),ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = V0a)))).
tff(conj_thm_2Erat_2ERAT__MUL__LID,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Erat_2Erat(V0a))) = V0a)))).
tff(conj_thm_2Erat_2ERAT__ADD__RINV,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0a)),ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0a)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Erat_2ERAT__ADD__LINV,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0a))),inj__ty_2Erat_2Erat(V0a))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Erat_2ERAT__MUL__RINV,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ((~~ (V0a = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0a)),ap(c_2Erat_2Erat__minv,inj__ty_2Erat_2Erat(V0a)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Erat_2ERAT__MUL__LINV,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ((~~ (V0a = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Erat__minv,inj__ty_2Erat_2Erat(V0a))),inj__ty_2Erat_2Erat(V0a))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Erat_2ERAT__RDISTRIB,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b))),inj__ty_2Erat_2Erat(V2c))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V2c))),ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V1b)),inj__ty_2Erat_2Erat(V2c)))))))))).
tff(conj_thm_2Erat_2ERAT__LDISTRIB,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V2c)),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b)))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V2c)),inj__ty_2Erat_2Erat(V0a))),ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V2c)),inj__ty_2Erat_2Erat(V1b)))))))))).
tff(conj_thm_2Erat_2ERAT__1__NOT__0,lemma,((~~ (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Erat_2ERAT__MUL__LZERO,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Erat_2ERAT__MUL__RZERO,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Erat_2ERAT__SUB__ADDAINV,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__DIV__MULMINV,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__div,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__minv,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__DIV__0,lemma,(( ! [V0x:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__div,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V0x))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Erat_2ERAT__AINV__0,lemma,((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Erat_2ERAT__AINV__AINV,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1)))) = V0r1)))).
tff(conj_thm_2Erat_2ERAT__AINV__ADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__AINV__SUB,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1)))))))).
tff(conj_thm_2Erat_2ERAT__AINV__RMUL,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__AINV__LMUL,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1))),inj__ty_2Erat_2Erat(V1r2)))))))).
tff(conj_thm_2Erat_2ERAT__AINV__EQ,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1))) = V1r2) <=> (V0r1 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__EQ__AINV,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V1r2)))) <=> (V0r1 = V1r2)))))).
tff(conj_thm_2Erat_2ERAT__AINV__MINV,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ((~~ (V0r1 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Erat__minv,inj__ty_2Erat_2Erat(V0r1)))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__minv,ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1))))))))).
tff(conj_thm_2Erat_2ERAT__SUB__RDISTRIB,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b))),inj__ty_2Erat_2Erat(V2c))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V2c))),ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V1b)),inj__ty_2Erat_2Erat(V2c)))))))))).
tff(conj_thm_2Erat_2ERAT__SUB__LDISTRIB,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V2c)),ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b)))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V2c)),inj__ty_2Erat_2Erat(V0a))),ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V2c)),inj__ty_2Erat_2Erat(V1b)))))))))).
tff(conj_thm_2Erat_2ERAT__SUB__LID,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1))))))).
tff(conj_thm_2Erat_2ERAT__SUB__RID,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0r1)))).
tff(conj_thm_2Erat_2ERAT__SUB__ID,lemma,(( ! [V0r:tp__ty_2Erat_2Erat] : (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r)),inj__ty_2Erat_2Erat(V0r))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Erat_2ERAT__EQ__SUB0,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (V0r1 = V1r2)))))).
tff(conj_thm_2Erat_2ERAT__EQ__0SUB,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))) <=> (V0r1 = V1r2)))))).
tff(conj_thm_2Erat_2ERAT__SGN__CALCULATE,lemma,(( ! [V0f1:tp__ty_2Efrac_2Efrac] : (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,ap(c_2Erat_2Eabs__rat,inj__ty_2Efrac_2Efrac(V0f1)))) = surj__ty_2Einteger_2Eint(ap(c_2Efrac_2Efrac__sgn,inj__ty_2Efrac_2Efrac(V0f1))))))).
tff(conj_thm_2Erat_2ERAT__SGN__CLAUSES,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (((surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) <=> p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (((surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (V0r1 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & ((surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> p(ap(ap(c_2Erat_2Erat__gre,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Erat_2ERAT__SGN__0,lemma,((surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Erat_2ERAT__SGN__AINV,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Erat_2Erat__sgn,ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1))))) = surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))))))).
tff(conj_thm_2Erat_2ERAT__SGN__MUL,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__SGN__MINV,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ((~~ (V0r1 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,ap(c_2Erat_2Erat__minv,inj__ty_2Erat_2Erat(V0r1)))) = surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1)))))))).
tff(conj_thm_2Erat_2ERAT__SGN__TOTAL,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ((surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) | ((surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) | (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))).
tff(conj_thm_2Erat_2ERAT__SGN__COMPLEMENT,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (((~~ (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) <=> ((surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) | (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & (((~~ (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) <=> ((surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) | (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) <=> ((surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) | (surj__ty_2Einteger_2Eint(ap(c_2Erat_2Erat__sgn,inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))))).
tff(conj_thm_2Erat_2ERAT__LES__REF,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : (~~ p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V0r1))))))).
tff(conj_thm_2Erat_2ERAT__LES__ANTISYM,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) => (~~ p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1))))))))).
tff(conj_thm_2Erat_2ERAT__LES__TRANS,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) & p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))) => p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V2r3))))))))).
tff(conj_thm_2Erat_2ERAT__LES__TOTAL,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) | ((V0r1 = V1r2) | p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1))))))))).
tff(conj_thm_2Erat_2ERAT__LEQ__REF,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V0r1)))))).
tff(conj_thm_2Erat_2ERAT__LEQ__ANTISYM,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) & p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1)))) => (V0r1 = V1r2)))))).
tff(conj_thm_2Erat_2ERAT__LEQ__TRANS,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) & p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))) => p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V2r3))))))))).
tff(conj_thm_2Erat_2ERAT__LES__01,lemma,(p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Erat_2ERAT__LES__IMP__LEQ,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) => p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))))))).
tff(conj_thm_2Erat_2ERAT__LES__IMP__NEQ,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) => (~~ (V0r1 = V1r2))))))).
tff(conj_thm_2Erat_2ERAT__LEQ__LES,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((~~ p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1)))) <=> p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))))))).
tff(conj_thm_2Erat_2ERAT__LES__LEQ,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((~~ p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1)))) <=> p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))))))).
tff(conj_thm_2Erat_2ERAT__LES__LEQ2,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) <=> (p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) & (~~ p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1)))))))))).
tff(conj_thm_2Erat_2ERAT__LES__LEQ__TRANS,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : ((p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b))) & p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V1b)),inj__ty_2Erat_2Erat(V2c)))) => p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V2c))))))))).
tff(conj_thm_2Erat_2ERAT__LEQ__LES__TRANS,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : ((p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b))) & p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V1b)),inj__ty_2Erat_2Erat(V2c)))) => p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V2c))))))))).
tff(conj_thm_2Erat_2ERAT__0LES__0LES__ADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V0r1))) => (p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V1r2))) => p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))))))))).
tff(conj_thm_2Erat_2ERAT__LES0__LES0__ADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) => (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V1r2)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) => p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Erat_2ERAT__0LES__0LEQ__ADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V0r1))) => (p(ap(ap(c_2Erat_2Erat__leq,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erat_2Erat(V1r2))) => p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2)))))))))).
tff(conj_thm_2Erat_2ERAT__LES0__LEQ0__ADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) => (p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V1r2)),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) => p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))),ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Erat_2ERAT__LSUB__EQ,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) = V2r3) <=> (V0r1 = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))))))))).
tff(conj_thm_2Erat_2ERAT__RSUB__EQ,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((V0r1 = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))) <=> (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V2r3))) = V1r2))))))).
tff(conj_thm_2Erat_2ERAT__LDIV__EQ,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((~~ (V1r2 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => ((surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__div,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))) = V2r3) <=> (V0r1 = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3))))))))))).
tff(conj_thm_2Erat_2ERAT__RDIV__EQ,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((~~ (V2r3 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => ((V0r1 = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__div,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))) <=> (surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V2r3))) = V1r2)))))))).
tff(conj_thm_2Erat_2ERAT__AINV__ONE__ONE,lemma,(p(ap(c_2Ebool_2EONE__ONE(ty_2Erat_2Erat,ty_2Erat_2Erat),c_2Erat_2Erat__ainv)))).
tff(conj_thm_2Erat_2ERAT__ADD__ONE__ONE,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : p(ap(c_2Ebool_2EONE__ONE(ty_2Erat_2Erat,ty_2Erat_2Erat),ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1))))))).
tff(conj_thm_2Erat_2ERAT__MUL__ONE__ONE,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ((~~ (V0r1 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) <=> p(ap(c_2Ebool_2EONE__ONE(ty_2Erat_2Erat,ty_2Erat_2Erat),ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)))))))).
tff(conj_thm_2Erat_2ERAT__EQ__LADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V2r3)),inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V2r3)),inj__ty_2Erat_2Erat(V1r2)))) <=> (V0r1 = V1r2))))))).
tff(conj_thm_2Erat_2ERAT__EQ__RADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V2r3))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))) <=> (V0r1 = V1r2))))))).
tff(conj_thm_2Erat_2ERAT__EQ__RMUL,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((~~ (V2r3 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => ((surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V2r3))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))) <=> (V0r1 = V1r2)))))))).
tff(conj_thm_2Erat_2ERAT__EQ__LMUL,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((~~ (V2r3 = surj__ty_2Erat_2Erat(ap(c_2Erat_2Erat__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => ((surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V2r3)),inj__ty_2Erat_2Erat(V0r1))) = surj__ty_2Erat_2Erat(ap(ap(c_2Erat_2Erat__mul,inj__ty_2Erat_2Erat(V2r3)),inj__ty_2Erat_2Erat(V1r2)))) <=> (V0r1 = V1r2)))))))).
tff(conj_thm_2Erat_2ERAT__LES__RADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V2r3))),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))) <=> p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__LES__LADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V2r3)),inj__ty_2Erat_2Erat(V0r1))),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V2r3)),inj__ty_2Erat_2Erat(V1r2)))) <=> p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__LEQ__RADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V2r3))),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))) <=> p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__LEQ__LADD,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V2r3)),inj__ty_2Erat_2Erat(V0r1))),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V2r3)),inj__ty_2Erat_2Erat(V1r2)))) <=> p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__ADD__MONO,lemma,(( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : ( ! [V3d:tp__ty_2Erat_2Erat] : ((p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V1b))) & p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V2c)),inj__ty_2Erat_2Erat(V3d)))) => p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0a)),inj__ty_2Erat_2Erat(V2c))),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V1b)),inj__ty_2Erat_2Erat(V3d))))))))))).
tff(conj_thm_2Erat_2ERAT__LES__AINV,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V0r1))),ap(c_2Erat_2Erat__ainv,inj__ty_2Erat_2Erat(V1r2)))) <=> p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V0r1)))))))).
tff(conj_thm_2Erat_2ERAT__LSUB__LES,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))),inj__ty_2Erat_2Erat(V2r3))) <=> p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))))))))).
tff(conj_thm_2Erat_2ERAT__RSUB__LES,lemma,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__les,inj__ty_2Erat_2Erat(V0r1)),ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))) <=> p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V2r3))),inj__ty_2Erat_2Erat(V1r2))))))))).
tff(conj_thm_2Erat_2ERAT__LSUB__LEQ,conjecture,(( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : (p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__sub,inj__ty_2Erat_2Erat(V0r1)),inj__ty_2Erat_2Erat(V1r2))),inj__ty_2Erat_2Erat(V2r3))) <=> p(ap(ap(c_2Erat_2Erat__leq,inj__ty_2Erat_2Erat(V0r1)),ap(ap(c_2Erat_2Erat__add,inj__ty_2Erat_2Erat(V1r2)),inj__ty_2Erat_2Erat(V2r3)))))))))).
