+record excess_ : Type ≝ {
+ exc_exc:> excess_dual;
+ exc_ap_: apartness;
+ exc_with1: ap_carr exc_ap_ = exc_carr exc_exc
+}.
+
+definition exc_ap: excess_ → apartness.
+intro E; apply (mk_apartness E); unfold Type_OF_excess_;
+cases (exc_with1 E); simplify;
+[apply (ap_apart (exc_ap_ E));
+|apply ap_coreflexive;|apply ap_symmetric;|apply ap_cotransitive]
+qed.
+
+coercion cic:/matita/excess/exc_ap.con.
+
+interpretation "Excess excess_" 'nleq a b =
+ (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess_1.con _) a b).
+
+record excess : Type ≝ {
+ excess_carr:> excess_;
+ ap2exc: ∀y,x:excess_carr. y # x → y ≰ x ∨ x ≰ y;
+ exc2ap: ∀y,x:excess_carr.y ≰ x ∨ x ≰ y → y # x
+}.
+
+interpretation "Excess excess" 'nleq a b =
+ (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
+
+interpretation "Excess (dual) excess" 'ngeq a b =
+ (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
+
+definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y.
+
+definition le ≝ λE:excess_base.λa,b:E. ¬ (a ≰ b).
+
+interpretation "Excess less or equal than" 'leq a b =
+ (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
+
+interpretation "Excess less or equal than" 'geq a b =
+ (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
+
+lemma le_reflexive: ∀E.reflexive ? (le E).
+unfold reflexive; intros 3 (E x H); apply (exc_coreflexive ?? H);
+qed.
+
+lemma le_transitive: ∀E.transitive ? (le E).
+unfold transitive; intros 7 (E x y z H1 H2 H3); cases (exc_cotransitive ??? y H3) (H4 H4);
+[cases (H1 H4)|cases (H2 H4)]
+qed.