+record excess_ : Type ≝ {
+ exc_exc:> excess_base;
+ exc_ap: apartness;
+ exc_with: ap_carr exc_ap = exc_carr exc_exc
+}.
+
+definition apart_of_excess_: excess_ → apartness.
+intro E; apply (mk_apartness E); unfold Type_OF_excess_;
+cases (exc_with E); simplify;
+[apply (ap_apart (exc_ap E));
+|apply ap_coreflexive;|apply ap_symmetric;|apply ap_cotransitive]
+qed.
+
+coercion cic:/matita/excess/apart_of_excess_.con.
+
+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
+}.
+
+definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y.
+
+definition le ≝ λE:excess.λa,b:E. ¬ (a ≰ b).
+
+interpretation "ordered sets less or equal than" 'leq a b =
+ (cic:/matita/excess/le.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.