set "baseuri" "cic:/matita/CoRN-Decl/reals/Bridges_LUB".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* begin hide *)
inline "cic:/CoRN/reals/Bridges_LUB/dcotrans_analyze_strong.con".
+(* NOTATION
+Notation "( p , q )" := (pairT p q).
+*)
+
inline "cic:/CoRN/reals/Bridges_LUB/dif_cotrans.con".
inline "cic:/CoRN/reals/Bridges_LUB/dif_cotrans_strong.con".