-(* 3.26 *)
-lemma ankS:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
- ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
-intros (R ml xn k n); elim n; simplify; [apply meet_comm]
-simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
-apply (Eq≈ ? (meet_assoc ????));
-apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
-apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-apply meet_comm;
-qed.
-
-
-
\ No newline at end of file
+notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $s $x}.
+notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $s $x}.
+notation < "s \nbsp 'is_increasing'" non associative with precedence 50 for @{'increasing $s}.
+notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 for @{'decreasing $s}.
+notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 50 for @{'strong_sup $s $x}.
+notation < "x \nbsp 'is_strong_inf' \nbsp s" non associative with precedence 50 for @{'strong_inf $s $x}.
+
+notation > "x 'is_upper_bound' s" non associative with precedence 50 for @{'upper_bound $s $x}.
+notation > "x 'is_lower_bound' s" non associative with precedence 50 for @{'lower_bound $s $x}.
+notation > "s 'is_increasing'" non associative with precedence 50 for @{'increasing $s}.
+notation > "s 'is_decreasing'" non associative with precedence 50 for @{'decreasing $s}.
+notation > "x 'is_strong_sup' s" non associative with precedence 50 for @{'strong_sup $s $x}.
+notation > "x 'is_strong_inf' s" non associative with precedence 50 for @{'strong_inf $s $x}.
+
+interpretation "Excess upper bound" 'upper_bound s x = (cic:/matita/infsup/upper_bound.con _ s x).
+interpretation "Excess lower bound" 'lower_bound s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con _) s x).
+interpretation "Excess increasing" 'increasing s = (cic:/matita/infsup/increasing.con _ s).
+interpretation "Excess decreasing" 'decreasing s = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con _) s).
+interpretation "Excess strong sup" 'strong_sup s x = (cic:/matita/infsup/strong_sup.con _ s x).
+interpretation "Excess strong inf" 'strong_inf s x = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con _) s x).
+
+definition seq_dual_exc_hint: ∀E.sequence E → sequence (dual_exc E) ≝ λE.λx:sequence E.x.
+definition seq_dual_exc_hint1: ∀E.sequence (dual_exc E) → sequence E ≝ λE.λx:sequence (dual_exc E).x.
+
+coercion cic:/matita/infsup/seq_dual_exc_hint.con nocomposites.
+coercion cic:/matita/infsup/seq_dual_exc_hint1.con nocomposites.