include('Axioms/nets^2.ax').
thf(tp_ty_2Erat_2Erat,type,( ty_2Erat_2Erat:del )).
thf(stp_ty_2Erat_2Erat,type,(tp__ty_2Erat_2Erat : $tType)).
thf(stp_inj_ty_2Erat_2Erat,type,(inj__ty_2Erat_2Erat : (tp__ty_2Erat_2Erat > $i))).
thf(stp_surj_ty_2Erat_2Erat,type,(surj__ty_2Erat_2Erat : ($i > tp__ty_2Erat_2Erat))).
thf(stp_inj_surj_ty_2Erat_2Erat,axiom,( ! [X:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (inj__ty_2Erat_2Erat @ X)) = X))).
thf(stp_inj_mem_ty_2Erat_2Erat,axiom,( ! [X:tp__ty_2Erat_2Erat] : (mem @ (inj__ty_2Erat_2Erat @ X) @ ty_2Erat_2Erat))).
thf(stp_iso_mem_ty_2Erat_2Erat,axiom,( ! [X:$i] : ((mem @ X @ ty_2Erat_2Erat) => (X = (inj__ty_2Erat_2Erat @ (surj__ty_2Erat_2Erat @ X)))))).
thf(tp_c_2Erat_2ERATD,type,(c_2Erat_2ERATD:$i)).
thf(mem_c_2Erat_2ERATD,axiom,(mem@c_2Erat_2ERATD@(arr@ty_2Erat_2Erat@ty_2Enum_2Enum))).
thf(stp_fo_c_2Erat_2ERATD,type,(fo__c_2Erat_2ERATD:(tp__ty_2Erat_2Erat > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Erat_2ERATN,type,(c_2Erat_2ERATN:$i)).
thf(mem_c_2Erat_2ERATN,axiom,(mem@c_2Erat_2ERATN@(arr@ty_2Erat_2Erat@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Erat_2ERATN,type,(fo__c_2Erat_2ERATN:(tp__ty_2Erat_2Erat > tp__ty_2Einteger_2Eint))).
thf(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))))).
thf(tp_c_2Erat_2Eabs__rat,type,(c_2Erat_2Eabs__rat:$i)).
thf(mem_c_2Erat_2Eabs__rat,axiom,(mem@c_2Erat_2Eabs__rat@(arr@ty_2Efrac_2Efrac@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Eabs__rat,type,(fo__c_2Erat_2Eabs__rat:(tp__ty_2Efrac_2Efrac > tp__ty_2Erat_2Erat))).
thf(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))))).
thf(tp_c_2Erat_2Eabs__rat__CLASS,type,(c_2Erat_2Eabs__rat__CLASS:$i)).
thf(mem_c_2Erat_2Eabs__rat__CLASS,axiom,(mem@c_2Erat_2Eabs__rat__CLASS@(arr@(arr@ty_2Efrac_2Efrac@bool)@ty_2Erat_2Erat))).
thf(tp_c_2Erat_2Erat__0,type,(c_2Erat_2Erat__0:$i)).
thf(mem_c_2Erat_2Erat__0,axiom,(mem@c_2Erat_2Erat__0@ty_2Erat_2Erat)).
thf(stp_fo_c_2Erat_2Erat__0,type,(fo__c_2Erat_2Erat__0:tp__ty_2Erat_2Erat)).
thf(stp_eq_fo_c_2Erat_2Erat__0,axiom,((inj__ty_2Erat_2Erat @ fo__c_2Erat_2Erat__0) = c_2Erat_2Erat__0)).
thf(tp_c_2Erat_2Erat__1,type,(c_2Erat_2Erat__1:$i)).
thf(mem_c_2Erat_2Erat__1,axiom,(mem@c_2Erat_2Erat__1@ty_2Erat_2Erat)).
thf(stp_fo_c_2Erat_2Erat__1,type,(fo__c_2Erat_2Erat__1:tp__ty_2Erat_2Erat)).
thf(stp_eq_fo_c_2Erat_2Erat__1,axiom,((inj__ty_2Erat_2Erat @ fo__c_2Erat_2Erat__1) = c_2Erat_2Erat__1)).
thf(tp_c_2Erat_2Erat__add,type,(c_2Erat_2Erat__add:$i)).
thf(mem_c_2Erat_2Erat__add,axiom,(mem@c_2Erat_2Erat__add@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__add,type,(fo__c_2Erat_2Erat__add:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(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)))))).
thf(tp_c_2Erat_2Erat__ainv,type,(c_2Erat_2Erat__ainv:$i)).
thf(mem_c_2Erat_2Erat__ainv,axiom,(mem@c_2Erat_2Erat__ainv@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Erat__ainv,type,(fo__c_2Erat_2Erat__ainv:(tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat))).
thf(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))))).
thf(tp_c_2Erat_2Erat__cons,type,(c_2Erat_2Erat__cons:$i)).
thf(mem_c_2Erat_2Erat__cons,axiom,(mem@c_2Erat_2Erat__cons@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__cons,type,(fo__c_2Erat_2Erat__cons:(tp__ty_2Einteger_2Eint > (tp__ty_2Einteger_2Eint > tp__ty_2Erat_2Erat)))).
thf(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)))))).
thf(tp_c_2Erat_2Erat__div,type,(c_2Erat_2Erat__div:$i)).
thf(mem_c_2Erat_2Erat__div,axiom,(mem@c_2Erat_2Erat__div@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__div,type,(fo__c_2Erat_2Erat__div:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(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)))))).
thf(tp_c_2Erat_2Erat__dnm,type,(c_2Erat_2Erat__dnm:$i)).
thf(mem_c_2Erat_2Erat__dnm,axiom,(mem@c_2Erat_2Erat__dnm@(arr@ty_2Erat_2Erat@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Erat_2Erat__dnm,type,(fo__c_2Erat_2Erat__dnm:(tp__ty_2Erat_2Erat > tp__ty_2Einteger_2Eint))).
thf(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))))).
thf(tp_c_2Erat_2Erat__equiv,type,(c_2Erat_2Erat__equiv:$i)).
thf(mem_c_2Erat_2Erat__equiv,axiom,(mem@c_2Erat_2Erat__equiv@(arr@ty_2Efrac_2Efrac@(arr@ty_2Efrac_2Efrac@bool)))).
thf(tp_c_2Erat_2Erat__geq,type,(c_2Erat_2Erat__geq:$i)).
thf(mem_c_2Erat_2Erat__geq,axiom,(mem@c_2Erat_2Erat__geq@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@bool)))).
thf(tp_c_2Erat_2Erat__gre,type,(c_2Erat_2Erat__gre:$i)).
thf(mem_c_2Erat_2Erat__gre,axiom,(mem@c_2Erat_2Erat__gre@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@bool)))).
thf(tp_c_2Erat_2Erat__leq,type,(c_2Erat_2Erat__leq:$i)).
thf(mem_c_2Erat_2Erat__leq,axiom,(mem@c_2Erat_2Erat__leq@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@bool)))).
thf(tp_c_2Erat_2Erat__les,type,(c_2Erat_2Erat__les:$i)).
thf(mem_c_2Erat_2Erat__les,axiom,(mem@c_2Erat_2Erat__les@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@bool)))).
thf(tp_c_2Erat_2Erat__max,type,(c_2Erat_2Erat__max:$i)).
thf(mem_c_2Erat_2Erat__max,axiom,(mem@c_2Erat_2Erat__max@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__max,type,(fo__c_2Erat_2Erat__max:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(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)))))).
thf(tp_c_2Erat_2Erat__min,type,(c_2Erat_2Erat__min:$i)).
thf(mem_c_2Erat_2Erat__min,axiom,(mem@c_2Erat_2Erat__min@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__min,type,(fo__c_2Erat_2Erat__min:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(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)))))).
thf(tp_c_2Erat_2Erat__minv,type,(c_2Erat_2Erat__minv:$i)).
thf(mem_c_2Erat_2Erat__minv,axiom,(mem@c_2Erat_2Erat__minv@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Erat__minv,type,(fo__c_2Erat_2Erat__minv:(tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat))).
thf(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))))).
thf(tp_c_2Erat_2Erat__mul,type,(c_2Erat_2Erat__mul:$i)).
thf(mem_c_2Erat_2Erat__mul,axiom,(mem@c_2Erat_2Erat__mul@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__mul,type,(fo__c_2Erat_2Erat__mul:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(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)))))).
thf(tp_c_2Erat_2Erat__nmr,type,(c_2Erat_2Erat__nmr:$i)).
thf(mem_c_2Erat_2Erat__nmr,axiom,(mem@c_2Erat_2Erat__nmr@(arr@ty_2Erat_2Erat@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Erat_2Erat__nmr,type,(fo__c_2Erat_2Erat__nmr:(tp__ty_2Erat_2Erat > tp__ty_2Einteger_2Eint))).
thf(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))))).
thf(tp_c_2Erat_2Erat__of__int,type,(c_2Erat_2Erat__of__int:$i)).
thf(mem_c_2Erat_2Erat__of__int,axiom,(mem@c_2Erat_2Erat__of__int@(arr@ty_2Einteger_2Eint@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Erat__of__int,type,(fo__c_2Erat_2Erat__of__int:(tp__ty_2Einteger_2Eint > tp__ty_2Erat_2Erat))).
thf(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))))).
thf(tp_c_2Erat_2Erat__of__num,type,(c_2Erat_2Erat__of__num:$i)).
thf(mem_c_2Erat_2Erat__of__num,axiom,(mem@c_2Erat_2Erat__of__num@(arr@ty_2Enum_2Enum@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Erat__of__num,type,(fo__c_2Erat_2Erat__of__num:(tp__ty_2Enum_2Enum > tp__ty_2Erat_2Erat))).
thf(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))))).
thf(tp_c_2Erat_2Erat__sgn,type,(c_2Erat_2Erat__sgn:$i)).
thf(mem_c_2Erat_2Erat__sgn,axiom,(mem@c_2Erat_2Erat__sgn@(arr@ty_2Erat_2Erat@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Erat_2Erat__sgn,type,(fo__c_2Erat_2Erat__sgn:(tp__ty_2Erat_2Erat > tp__ty_2Einteger_2Eint))).
thf(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))))).
thf(tp_c_2Erat_2Erat__sub,type,(c_2Erat_2Erat__sub:$i)).
thf(mem_c_2Erat_2Erat__sub,axiom,(mem@c_2Erat_2Erat__sub@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__sub,type,(fo__c_2Erat_2Erat__sub:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(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)))))).
thf(tp_c_2Erat_2Erep__rat,type,(c_2Erat_2Erep__rat:$i)).
thf(mem_c_2Erat_2Erep__rat,axiom,(mem@c_2Erat_2Erep__rat@(arr@ty_2Erat_2Erat@ty_2Efrac_2Efrac))).
thf(stp_fo_c_2Erat_2Erep__rat,type,(fo__c_2Erat_2Erep__rat:(tp__ty_2Erat_2Erat > tp__ty_2Efrac_2Efrac))).
thf(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))))).
thf(tp_c_2Erat_2Erep__rat__CLASS,type,(c_2Erat_2Erep__rat__CLASS:$i)).
thf(mem_c_2Erat_2Erep__rat__CLASS,axiom,(mem@c_2Erat_2Erep__rat__CLASS@(arr@ty_2Erat_2Erat@(arr@ty_2Efrac_2Efrac@bool)))).
thf(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))))))))).
thf(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))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))))).
thf(conj_thm_2Erat_2ERAT__EQUIV__ALT,lemma,( ! [V0a:tp__ty_2Efrac_2Efrac] : ((ap@c_2Erat_2Erat__equiv@(inj__ty_2Efrac_2Efrac @ V0a)) = (lam@ty_2Efrac_2Efrac@(^ [V1x:$i] : (ap@(c_2Ebool_2E_3F@ty_2Einteger_2Eint)@(lam@ty_2Einteger_2Eint@(^ [V2b:$i] : (ap@(c_2Ebool_2E_3F@ty_2Einteger_2Eint)@(lam@ty_2Einteger_2Eint@(^ [V3c:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@V2b))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@V3c))@(ap@(ap@(c_2Emin_2E_3D@ty_2Efrac_2Efrac)@(ap@(ap@c_2Efrac_2Efrac__mul@(inj__ty_2Efrac_2Efrac @ V0a))@(ap@c_2Efrac_2Eabs__frac@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@V2b)@V2b))))@(ap@(ap@c_2Efrac_2Efrac__mul@V1x)@(ap@c_2Efrac_2Eabs__frac@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@V3c)@V3c))))))))))))))))).
thf(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)@(lam@(arr@ty_2Efrac_2Efrac@bool)@(^ [V1c:$i] : (ap@(c_2Ebool_2E_3F@ty_2Efrac_2Efrac)@(lam@ty_2Efrac_2Efrac@(^ [V2r:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Erat_2Erat__equiv@V2r)@V2r))@(ap@(ap@(c_2Emin_2E_3D@(arr@ty_2Efrac_2Efrac@bool))@V1c)@(ap@c_2Erat_2Erat__equiv@V2r)))))))))@V0rep))))).
thf(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@(lam@(arr@ty_2Efrac_2Efrac@bool)@(^ [V2c:$i] : (ap@(c_2Ebool_2E_3F@ty_2Efrac_2Efrac)@(lam@ty_2Efrac_2Efrac@(^ [V3r:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Erat_2Erat__equiv@V3r)@V3r))@(ap@(ap@(c_2Emin_2E_3D@(arr@ty_2Efrac_2Efrac@bool))@V2c)@(ap@c_2Erat_2Erat__equiv@V3r))))))))@V1r)) <=> ((ap@c_2Erat_2Erep__rat__CLASS@(ap@c_2Erat_2Eabs__rat__CLASS@V1r)) = V1r)))))).
thf(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)))))).
thf(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))))))).
thf(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))))))).
thf(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))).
thf(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))).
thf(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))))))))).
thf(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))))).
thf(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))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))).
thf(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))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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))))))).
thf(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)))))).
thf(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))))))).
thf(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)))))))))).
thf(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)))@(lam@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool))@(^ [V0R:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Erelation_2EWF@ty_2Enum_2Enum)@V0R))@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@V0R@(ap@c_2Enum_2ESUC@V1n))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@V1n)))))))))))@(lam@(arr@ty_2Enum_2Enum@ty_2Erat_2Erat)@(^ [V2rat__of__num:$i] : (lam@ty_2Enum_2Enum@(^ [V3a:$i] : (ap@(ap@(ap@(c_2Earithmetic_2Enum__CASE@ty_2Erat_2Erat)@V3a)@(ap@(c_2Ecombin_2EI@ty_2Erat_2Erat)@(inj__ty_2Erat_2Erat @ fo__c_2Erat_2Erat__0)))@(lam@ty_2Enum_2Enum@(^ [V4v:$i] : (ap@(ap@(ap@(c_2Earithmetic_2Enum__CASE@ty_2Erat_2Erat)@V4v)@(ap@(c_2Ecombin_2EI@ty_2Erat_2Erat)@(inj__ty_2Erat_2Erat @ fo__c_2Erat_2Erat__1)))@(lam@ty_2Enum_2Enum@(^ [V5n:$i] : (ap@(c_2Ecombin_2EI@ty_2Erat_2Erat)@(ap@(ap@c_2Erat_2Erat__add@(ap@V2rat__of__num@(ap@c_2Enum_2ESUC@V5n)))@(inj__ty_2Erat_2Erat @ fo__c_2Erat_2Erat__1)))))))))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))).
thf(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))))).
thf(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))).
thf(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))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))).
thf(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))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))).
thf(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))))))).
thf(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))).
thf(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))).
thf(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))).
thf(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))).
thf(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)))))).
thf(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)))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))).
thf(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)))))).
thf(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)))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))).
thf(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))))).
thf(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))).
thf(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)))))))).
thf(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))))))).
thf(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)))))))).
thf(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))))))).
thf(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)))))))).
thf(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))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))).
thf(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))).
thf(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)))))).
thf(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))))).
thf(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))))).
thf(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)))))).
thf(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))))))))).
thf(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))))).
thf(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)))))).
thf(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)))))))).
thf(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))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))).
thf(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))))).
thf(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)))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))).
thf(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))))))).
thf(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))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))).
thf(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)))))))))).
thf(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))))))).
thf(conj_thm_2Erat_2ERAT__AINV__ONE__ONE,lemma,(p@(ap@(c_2Ebool_2EONE__ONE@ty_2Erat_2Erat@ty_2Erat_2Erat)@c_2Erat_2Erat__ainv))).
thf(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)))))).
thf(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))))))).
thf(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)))))).
thf(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)))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))))).
thf(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))))))).
thf(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))))))))).
thf(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)))))))).
thf(conj_thm_2Erat_2ERAT__LSUB__LEQ,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__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))))))))).
thf(conj_thm_2Erat_2ERAT__RSUB__LEQ,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))@(ap@(ap@c_2Erat_2Erat__sub@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))) <=> (p@(ap@(ap@c_2Erat_2Erat__leq@(ap@(ap@c_2Erat_2Erat__add@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3)))@(inj__ty_2Erat_2Erat @ V1r2)))))))).
thf(conj_thm_2Erat_2ERAT__LES__RMUL__POS,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3: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 @ V2r3))) => ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3)))@(ap@(ap@c_2Erat_2Erat__mul@(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))))))))).
thf(conj_thm_2Erat_2ERAT__LES__LMUL__POS,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3: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 @ V2r3))) => ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V2r3))@(inj__ty_2Erat_2Erat @ V0r1)))@(ap@(ap@c_2Erat_2Erat__mul@(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))))))))).
thf(conj_thm_2Erat_2ERAT__LES__RMUL__NEG,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 @ V2r3))@(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__mul@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3)))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))))))))).
thf(conj_thm_2Erat_2ERAT__LES__LMUL__NEG,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 @ V2r3))@(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__mul@(inj__ty_2Erat_2Erat @ V2r3))@(inj__ty_2Erat_2Erat @ V1r2)))@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V2r3))@(inj__ty_2Erat_2Erat @ V0r1)))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))))))))).
thf(conj_thm_2Erat_2ERAT__AINV__LES,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)))@(inj__ty_2Erat_2Erat @ V1r2))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V1r2)))@(inj__ty_2Erat_2Erat @ V0r1))))))).
thf(conj_thm_2Erat_2ERAT__LDIV__LES__POS,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3: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 @ V1r2))) => ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@(ap@c_2Erat_2Erat__div@(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__mul@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))))))))).
thf(conj_thm_2Erat_2ERAT__LDIV__LES__NEG,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 @ 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__div@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2)))@(inj__ty_2Erat_2Erat @ V2r3))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))@(inj__ty_2Erat_2Erat @ V0r1))))))))).
thf(conj_thm_2Erat_2ERAT__RDIV__LES__POS,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3: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 @ V2r3))) => ((p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0r1))@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3)))@(inj__ty_2Erat_2Erat @ V1r2))))))))).
thf(conj_thm_2Erat_2ERAT__RDIV__LES__NEG,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 @ V2r3))@(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 @ V0r1))@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V1r2))@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3)))))))))).
thf(conj_thm_2Erat_2ERAT__LDIV__LEQ__POS,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3: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 @ V1r2))) => ((p@(ap@(ap@c_2Erat_2Erat__leq@(ap@(ap@c_2Erat_2Erat__div@(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__mul@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))))))))).
thf(conj_thm_2Erat_2ERAT__LDIV__LEQ__NEG,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 @ V1r2))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) => ((p@(ap@(ap@c_2Erat_2Erat__leq@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2)))@(inj__ty_2Erat_2Erat @ V2r3))) <=> (p@(ap@(ap@c_2Erat_2Erat__leq@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))@(inj__ty_2Erat_2Erat @ V0r1))))))))).
thf(conj_thm_2Erat_2ERAT__RDIV__LEQ__POS,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3: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 @ V2r3))) => ((p@(ap@(ap@c_2Erat_2Erat__leq@(inj__ty_2Erat_2Erat @ V0r1))@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))) <=> (p@(ap@(ap@c_2Erat_2Erat__leq@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3)))@(inj__ty_2Erat_2Erat @ V1r2))))))))).
thf(conj_thm_2Erat_2ERAT__RDIV__LEQ__NEG,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 @ V2r3))@(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 @ V0r1))@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))) <=> (p@(ap@(ap@c_2Erat_2Erat__leq@(inj__ty_2Erat_2Erat @ V1r2))@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3)))))))))).
thf(conj_thm_2Erat_2ERAT__LES__SUB0,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2: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)))@(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 @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))))))).
thf(conj_thm_2Erat_2ERAT__LES__0SUB,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)))@(ap@(ap@c_2Erat_2Erat__sub@(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))))))).
thf(conj_thm_2Erat_2ERAT__MINV__LES,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_2Erat_2Erat__les@(ap@c_2Erat_2Erat__minv@(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 @ V0r1))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((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__minv@(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 @ V0r1)))))))).
thf(conj_thm_2Erat_2ERAT__MUL__SIGN__CASES,lemma,( ! [V0p:tp__ty_2Erat_2Erat] : ( ! [V1q: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)))@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0p))@(inj__ty_2Erat_2Erat @ V1q)))) <=> (((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 @ V0p))) & (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 @ V1q)))) | ((p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0p))@(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 @ V1q))@(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__mul@(inj__ty_2Erat_2Erat @ V0p))@(inj__ty_2Erat_2Erat @ V1q)))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (((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 @ V0p))) & (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V1q))@(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 @ V0p))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (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 @ V1q)))))))))).
thf(conj_thm_2Erat_2ERAT__NO__ZERODIV,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (((V0r1 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) | (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__mul@(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)))))))).
thf(conj_thm_2Erat_2ERAT__NO__ZERODIV__THM,lemma,( ! [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_2Erat__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)))) | (V1r2 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))).
thf(conj_thm_2Erat_2ERAT__NO__ZERODIV__NEG,lemma,( ! [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_2Erat__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))))) & (~~ (V1r2 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(conj_thm_2Erat_2ERAT__NO__IDDIV,lemma,( ! [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))) = V1r2) <=> ((V0r1 = (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)))))) | (V1r2 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))).
thf(conj_thm_2Erat_2ERDIV__MUL__OUT,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__mul@(inj__ty_2Erat_2Erat @ V0r1))@(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__div@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2)))@(inj__ty_2Erat_2Erat @ V2r3)))))))).
thf(conj_thm_2Erat_2ELDIV__MUL__OUT,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__mul@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2)))@(inj__ty_2Erat_2Erat @ V2r3))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3)))@(inj__ty_2Erat_2Erat @ V1r2)))))))).
thf(conj_thm_2Erat_2ERAT__DENSE__THM,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r3:tp__ty_2Erat_2Erat] : ((p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r3))) => (? [V2r2:tp__ty_2Erat_2Erat] : ((p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r2))) & (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V2r2))@(inj__ty_2Erat_2Erat @ V1r3))))))))).
thf(conj_thm_2Erat_2ERAT__SAVE,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : (? [V1a1:tp__ty_2Einteger_2Eint] : (? [V2b1:tp__ty_2Enum_2Enum] : (V0r1 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(ap@(ap@c_2Efrac_2Efrac__save@(inj__ty_2Einteger_2Eint @ V1a1))@(inj__ty_2Enum_2Enum @ V2b1))))))))).
thf(conj_thm_2Erat_2ERAT__SAVE__MINV,lemma,( ! [V0a1:tp__ty_2Einteger_2Eint] : ( ! [V1b1:tp__ty_2Enum_2Enum] : ((~~ ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(ap@(ap@c_2Efrac_2Efrac__save@(inj__ty_2Einteger_2Eint @ V0a1))@(inj__ty_2Enum_2Enum @ V1b1)))) = (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__minv@(ap@c_2Erat_2Eabs__rat@(ap@(ap@c_2Efrac_2Efrac__save@(inj__ty_2Einteger_2Eint @ V0a1))@(inj__ty_2Enum_2Enum @ V1b1))))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(ap@(ap@c_2Efrac_2Efrac__save@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2EintExtension_2ESGN@(inj__ty_2Einteger_2Eint @ V0a1)))@(ap@(ap@c_2Einteger_2Eint__add@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1b1)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@c_2Einteger_2ENum@(ap@(ap@c_2Einteger_2Eint__sub@(ap@c_2Einteger_2EABS@(inj__ty_2Einteger_2Eint @ V0a1)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))).
thf(conj_thm_2Erat_2ERAT__SAVE__TO__CONS,lemma,( ! [V0a1:tp__ty_2Einteger_2Eint] : ( ! [V1b1:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(ap@(ap@c_2Efrac_2Efrac__save@(inj__ty_2Einteger_2Eint @ V0a1))@(inj__ty_2Enum_2Enum @ V1b1)))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__cons@(inj__ty_2Einteger_2Eint @ V0a1))@(ap@(ap@c_2Einteger_2Eint__add@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1b1)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(conj_thm_2Erat_2ERAT__OF__NUM,lemma,( ! [A_27a:del]: ( ! [V0n:$i] : ((mem@V0n@A_27a) => (((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Erat_2Erat__0) & ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Erat_2Erat @ fo__c_2Erat_2Erat__1)))))))))).
thf(conj_thm_2Erat_2ERAT__SAVE__NUM,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(ap@(ap@c_2Efrac_2Efrac__save@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(conj_thm_2Erat_2ERAT__CONS__TO__NUM,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__cons@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Einteger_2Eint__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 @ V0n)))) & ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__cons@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0n))))@(ap@c_2Einteger_2Eint__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__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V0n)))))))).
thf(conj_thm_2Erat_2ERAT__0,lemma,(fo__c_2Erat_2Erat__0 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(conj_thm_2Erat_2ERAT__1,lemma,(fo__c_2Erat_2Erat__1 = (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))))))).
thf(conj_thm_2Erat_2ERAT__MINV__1,lemma,((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__minv@(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@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))).
thf(conj_thm_2Erat_2ERAT__DIV__1,lemma,( ! [V0r:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V0r))@(ap@c_2Erat_2Erat__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V0r))).
thf(conj_thm_2Erat_2ERAT__DIV__NEG1,lemma,( ! [V0r:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V0r))@(ap@c_2Erat_2Erat__ainv@(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__ainv@(inj__ty_2Erat_2Erat @ V0r)))))).
thf(conj_thm_2Erat_2ERAT__DIV__INV,lemma,( ! [V0r:tp__ty_2Erat_2Erat] : ((~~ (V0r = (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 @ V0r))@(inj__ty_2Erat_2Erat @ V0r))) = (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))))))))).
thf(conj_thm_2Erat_2ERAT__MINV__MUL,lemma,( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : (((~~ (V0a = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V1b = (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__minv@(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@(ap@c_2Erat_2Erat__minv@(inj__ty_2Erat_2Erat @ V0a)))@(ap@c_2Erat_2Erat__minv@(inj__ty_2Erat_2Erat @ V1b))))))))).
thf(conj_thm_2Erat_2ERAT__DIVDIV__MUL,lemma,( ! [V0b:tp__ty_2Erat_2Erat] : ( ! [V1d:tp__ty_2Erat_2Erat] : ( ! [V2a:tp__ty_2Erat_2Erat] : ( ! [V3c:tp__ty_2Erat_2Erat] : (((~~ (V0b = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V1d = (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@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V2a))@(inj__ty_2Erat_2Erat @ V0b)))@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V3c))@(inj__ty_2Erat_2Erat @ V1d)))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V2a))@(inj__ty_2Erat_2Erat @ V3c)))@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0b))@(inj__ty_2Erat_2Erat @ V1d))))))))))).
thf(conj_thm_2Erat_2ERAT__DIVDIV__ADD,lemma,( ! [V0y:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2x:tp__ty_2Erat_2Erat] : ( ! [V3a:tp__ty_2Erat_2Erat] : (((~~ (V0y = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V1b = (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__add@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V2x))@(inj__ty_2Erat_2Erat @ V0y)))@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V3a))@(inj__ty_2Erat_2Erat @ V1b)))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(ap@(ap@c_2Erat_2Erat__add@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V2x))@(inj__ty_2Erat_2Erat @ V1b)))@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V3a))@(inj__ty_2Erat_2Erat @ V0y))))@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0y))@(inj__ty_2Erat_2Erat @ V1b))))))))))).
thf(conj_thm_2Erat_2ERAT__DIV__AINV,lemma,( ! [V0x:tp__ty_2Erat_2Erat] : ( ! [V1y:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V0x))@(inj__ty_2Erat_2Erat @ V1y)))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V0x)))@(inj__ty_2Erat_2Erat @ V1y))))))).
thf(conj_thm_2Erat_2ERAT__MINV__EQ__0,lemma,( ! [V0r:tp__ty_2Erat_2Erat] : ((~~ (V0r = (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__minv@(inj__ty_2Erat_2Erat @ V0r))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))).
thf(conj_thm_2Erat_2ERAT__DIV__MINV,lemma,( ! [V0x:tp__ty_2Erat_2Erat] : ( ! [V1y:tp__ty_2Erat_2Erat] : (((~~ (V0x = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V1y = (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__minv@(ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V0x))@(inj__ty_2Erat_2Erat @ V1y)))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V1y))@(inj__ty_2Erat_2Erat @ V0x)))))))).
thf(conj_thm_2Erat_2ERAT__DIV__EQ0,lemma,( ! [V0d:tp__ty_2Erat_2Erat] : ( ! [V1n:tp__ty_2Erat_2Erat] : ((~~ (V0d = (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 @ V1n))@(inj__ty_2Erat_2Erat @ V0d))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (V1n = (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__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V1n))@(inj__ty_2Erat_2Erat @ V0d)))) <=> (V1n = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(conj_thm_2Erat_2ERAT__ADD__NUM__CALCULATE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V1m)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))))))) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2n))))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Erat_2Erat @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erat_2Erat)@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m)))@(ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V2n))))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m))))))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V4n)))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V5m))))) = (surj__ty_2Erat_2Erat @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erat_2Erat)@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V5m))@(inj__ty_2Enum_2Enum @ V4n)))@(ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V4n))@(inj__ty_2Enum_2Enum @ V5m))))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V5m))@(inj__ty_2Enum_2Enum @ V4n))))))))) & ( ! [V6n:tp__ty_2Enum_2Enum] : ( ! [V7m:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V6n))))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V7m))))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6n))@(inj__ty_2Enum_2Enum @ V7m)))))))))))).
thf(conj_thm_2Erat_2ERAT__MUL__NUM__CALCULATE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__mul@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V1m)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))))))) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__mul@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2n))))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m)))))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__mul@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V4n)))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V5m))))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V4n))@(inj__ty_2Enum_2Enum @ V5m)))))))) & ( ! [V6n:tp__ty_2Enum_2Enum] : ( ! [V7m:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__mul@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V6n))))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V7m))))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V6n))@(inj__ty_2Enum_2Enum @ V7m))))))))))).
thf(conj_thm_2Erat_2ERAT__EQ__NUM__CALCULATE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V1m)))) <=> (V0n = V1m)))) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : (((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2n))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V3m))))) <=> ((V2n = fo__c_2Enum_2E0) & (V3m = fo__c_2Enum_2E0))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : (((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V4n)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V5m)))) <=> ((V4n = fo__c_2Enum_2E0) & (V5m = fo__c_2Enum_2E0))))) & ( ! [V6n:tp__ty_2Enum_2Enum] : ( ! [V7m:tp__ty_2Enum_2Enum] : (((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V6n)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V7m))))) <=> (V6n = V7m)))))))).
thf(conj_thm_2Erat_2ERAT__LT__NUM__CALCULATE,lemma,( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n: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)))) & (((p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2m))))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V3n)))) <=> ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V2m))) | (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V3n))))) & (((p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2m)))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V3n))))) <=> $false) & ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2m))))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V3n))))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2Enum_2Enum @ V2m)))))))))))).
thf(conj_thm_2Erat_2ERAT__LE__NUM__CALCULATE,lemma,( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n: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)))) & (((p@(ap@(ap@c_2Erat_2Erat__leq@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2m))))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V3n)))) <=> $true) & (((p@(ap@(ap@c_2Erat_2Erat__leq@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2m)))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V3n))))) <=> ((V2m = fo__c_2Enum_2E0) & (V3n = fo__c_2Enum_2E0))) & ((p@(ap@(ap@c_2Erat_2Erat__leq@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2m))))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V3n))))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2Enum_2Enum @ V2m)))))))))))).
thf(ax_thm_2Erat_2Erat__of__int__def,axiom,( ! [V0i:tp__ty_2Einteger_2Eint] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V0i))) = (surj__ty_2Erat_2Erat @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erat_2Erat)@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V0i))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(ap@c_2Einteger_2ENum@(ap@c_2Einteger_2Eint__neg@(inj__ty_2Einteger_2Eint @ V0i))))))@(ap@c_2Erat_2Erat__of__num@(ap@c_2Einteger_2ENum@(inj__ty_2Einteger_2Eint @ V0i)))))))).
thf(conj_thm_2Erat_2Erat__of__int__11,lemma,( ! [V0i1:tp__ty_2Einteger_2Eint] : ( ! [V1i2:tp__ty_2Einteger_2Eint] : (((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V0i1))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V1i2)))) <=> (V0i1 = V1i2))))).
thf(conj_thm_2Erat_2Erat__of__int__of__num,lemma,( ! [V0x:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__int@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0x)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V0x)))))).
thf(conj_thm_2Erat_2Erat__of__int__MUL,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__mul@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V0x)))@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V1y)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__int@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V0x))@(inj__ty_2Einteger_2Eint @ V1y)))))))).
thf(conj_thm_2Erat_2Erat__of__int__ADD,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V0x)))@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V1y)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__int@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V0x))@(inj__ty_2Einteger_2Eint @ V1y)))))))).
thf(conj_thm_2Erat_2Erat__of__int__LE,lemma,( ! [V0i:tp__ty_2Einteger_2Eint] : ( ! [V1j:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Erat_2Erat__leq@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V0i)))@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V1j)))) <=> (p@(ap@(ap@c_2Einteger_2Eint__le@(inj__ty_2Einteger_2Eint @ V0i))@(inj__ty_2Einteger_2Eint @ V1j))))))).
thf(conj_thm_2Erat_2Erat__of__int__LT,lemma,( ! [V0i:tp__ty_2Einteger_2Eint] : ( ! [V1j:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V0i)))@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V1j)))) <=> (p@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V0i))@(inj__ty_2Einteger_2Eint @ V1j))))))).
thf(conj_thm_2Erat_2Erat__of__int__ainv,lemma,( ! [V0i:tp__ty_2Einteger_2Eint] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__int@(ap@c_2Einteger_2Eint__neg@(inj__ty_2Einteger_2Eint @ V0i)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V0i))))))).
thf(conj_thm_2Erat_2ERAT__OF__INT__CALCULATE,lemma,( ! [V0i:tp__ty_2Einteger_2Eint] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V0i))) = (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)@(inj__ty_2Einteger_2Eint @ V0i))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(ax_thm_2Erat_2ERATND__THM,axiom,( ! [V0r:tp__ty_2Erat_2Erat] : ((V0r = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(ap@c_2Erat_2Erat__of__int@(ap@c_2Erat_2ERATN@(inj__ty_2Erat_2Erat @ V0r))))@(ap@c_2Erat_2Erat__of__num@(ap@c_2Erat_2ERATD@(inj__ty_2Erat_2Erat @ V0r)))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Erat_2ERATD@(inj__ty_2Erat_2Erat @ V0r)))) & ((((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2ERATN@(inj__ty_2Erat_2Erat @ V0r))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) => ((surj__ty_2Enum_2Enum @ (ap@c_2Erat_2ERATD@(inj__ty_2Erat_2Erat @ V0r))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & ( ! [V1n_27:tp__ty_2Einteger_2Eint] : ( ! [V2d_27:tp__ty_2Enum_2Enum] : (((V0r = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V1n_27)))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2d_27))))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V2d_27)))) => (p@(ap@(ap@c_2Einteger_2Eint__le@(ap@c_2Einteger_2EABS@(ap@c_2Erat_2ERATN@(inj__ty_2Erat_2Erat @ V0r))))@(ap@c_2Einteger_2EABS@(inj__ty_2Einteger_2Eint @ V1n_27)))))))))))).
thf(conj_thm_2Erat_2ERATD__NZERO,conjecture,( ! [V0r:tp__ty_2Erat_2Erat] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Erat_2ERATD@(inj__ty_2Erat_2Erat @ V0r)))) & (~~ ((surj__ty_2Enum_2Enum @ (ap@c_2Erat_2ERATD@(inj__ty_2Erat_2Erat @ V0r))) = fo__c_2Enum_2E0))))).
