(* E(#,≰) → E(#,sym(≰)) *)
lemma make_dual_exc: excess_base → excess_base.
(* E(#,≰) → E(#,sym(≰)) *)
lemma make_dual_exc: excess_base → excess_base.
definition apartness_of_excess_base: excess_base → apartness.
intros (E); apply (mk_apartness E (λa,b:E. a ≰ b ∨ b ≰ a));
definition apartness_of_excess_base: excess_base → apartness.
intros (E); apply (mk_apartness E (λa,b:E. a ≰ b ∨ b ≰ a));
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 =
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 =
lemma le_reflexive: ∀E.reflexive ? (le E).
unfold reflexive; intros 3 (E x H); apply (exc_coreflexive ?? H);
lemma le_reflexive: ∀E.reflexive ? (le E).
unfold reflexive; intros 3 (E x H); apply (exc_coreflexive ?? H);
definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b).
notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}.
definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b).
notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}.
-interpretation "Apartness alikeness" 'napart a b = (cic:/matita/excess/eq.con _ a b).
-interpretation "Excess alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
-interpretation "Excess (dual) alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
+interpretation "Apartness alikeness" 'napart a b = (eq _ a b).
+interpretation "Excess alikeness" 'napart a b = (eq (excess_base_OF_excess1 _) a b).
+interpretation "Excess (dual) alikeness" 'napart a b = (eq (excess_base_OF_excess _) a b).
lemma eq_reflexive:∀E:apartness. reflexive ? (eq E).
intros (E); unfold; intros (x); apply ap_coreflexive;
lemma eq_reflexive:∀E:apartness. reflexive ? (eq E).
intros (E); unfold; intros (x); apply ap_coreflexive;
λE,x,y,z.eq_trans_ E x z y.
notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}.
λE,x,y,z.eq_trans_ E x z y.
notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}.
lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
alias symbol "napart" = "Apartness alikeness".
lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
alias symbol "napart" = "Apartness alikeness".
lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x.
intros (A x y z E H); split; elim H;
lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x.
intros (A x y z E H); split; elim H;
lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]
lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]