+interpretation "Excess base excess" 'nleq a b = (cic:/matita/excess/exc_excess.con _ a b).
+
+(* E(#,≰) → E(#,sym(≰)) *)
+lemma make_dual_exc: excess_base → excess_base.
+intro E;
+apply (mk_excess_base (exc_carr E));
+ [ apply (λx,y:E.y≰x);|apply exc_coreflexive;
+ | unfold cotransitive; simplify; intros (x y z H);
+ cases (exc_cotransitive E ??z H);[right|left]assumption]
+qed.
+
+record excess_dual : Type ≝ {
+ exc_dual_base:> excess_base;
+ exc_dual_dual_ : excess_base;
+ exc_with: exc_dual_dual_ = make_dual_exc exc_dual_base
+}.
+
+lemma mk_excess_dual_smart: excess_base → excess_dual.
+intro; apply mk_excess_dual; [apply e| apply (make_dual_exc e)|reflexivity]
+qed.
+
+definition exc_dual_dual: excess_dual → excess_base.
+intro E; apply (make_dual_exc E);
+qed.
+
+coercion cic:/matita/excess/exc_dual_dual.con.