-(* Definition 2.10 *)
-coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B.
-definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x].
-definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y].
-
-interpretation "pair pi1" 'pi1 x =
- (cic:/matita/dama/supremum/first.con _ _ x).
-interpretation "pair pi2" 'pi2 x =
- (cic:/matita/dama/supremum/second.con _ _ x).
-
-notation "hvbox(\langle a, break b\rangle)" non associative with precedence 91 for @{ 'pair $a $b}.
-interpretation "pair" 'pair a b =
- (cic:/matita/dama/supremum/pair.ind#xpointer(1/1/1) _ _ a b).
-
-notation "a \times b" left associative with precedence 60 for @{'prod $a $b}.
-interpretation "prod" 'prod a b =
- (cic:/matita/dama/supremum/pair.ind#xpointer(1/1) a b).
-
-lemma square_ordered_set: ordered_set → ordered_set.
-intro O; apply (mk_ordered_set (O × O));
-[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
-|2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
- cases H (X X); apply (os_coreflexive ?? X);
-|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);
- clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
- [1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
- |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
-qed.