proposition: Lemma Exercise1_10_ter (r':= canonical_doubleton_order) (r := order_product2 r' r') (f := Lf (fun z => (Yo (z = J C0 C0)) C0 C1) (C2 \times C2) C2): Exercise1_10_counterexample r r' f.
proof: Proof. move: cdo_wor => [cdo sr']. have l1: lattice r' by apply: total_order_lattice;apply: worder_total. have l2: lattice r by apply: product2_lattice. move: (l1)(l2) => [or1 _][or2 _]. have ta: lf_axiom (fun z => (Yo (z = J C0 C0)) C0 C1) (C2 \times C2) C2. move => z _; simpl; Ytac ww; fprops. have sr: substrate r = C2 \times C2. by rewrite order_product2_sr// -/r' sr'. have ff: function f by apply: lf_function. set c := J C0 C0. set a := J C0 C1. set b := J C1 C0. have nac: a <> c by move => ac; move: (pr2_def ac); fprops. have nbc: b <> c by move => ac; move: (pr1_def ac); fprops. have asr: inc a (substrate r) by rewrite sr /a; fprops. have bsr: inc b (substrate r) by rewrite sr /b; fprops. have csr: inc c (substrate r) by rewrite sr /c; fprops. have ic: (inf r a b) = c. move: (lattice_inf_pr l2 asr bsr) => [] /order_product2_P [itp _ [r1 r2]] /order_product2_P [_ _ [r3 r4]] _. rewrite - (setX_pair itp). move: r1 => /cdo_gleP;case. move => [-> _]; move: r4 => /cdo_gleP; case; first by move => [-> _]. by move => [_]; rewrite/b;aw => sv; case: C0_ne_C1. by move => [_]; rewrite/b;aw => sv; case: C0_ne_C1. by move => [_];rewrite/a; aw => sv; case: C0_ne_C1. by move => [_];rewrite/a; aw => sv; case: C0_ne_C1. have fp: function_prop f (substrate r) (substrate r') by rewrite /f;split; aw. saw; first split => //. move=> x y; move /order_product2_P; rewrite sr'. rewrite /f;move=> [xp yp [le1 le2]]; rewrite !LfV//. apply /cdo_gleP => //;Ytac xm; Ytac ym; try in_TP4; case: xm. rewrite - (setX_pair xp); move: le1 => /cdo_gleP; case. + move => [-> _]; move: le2 => /cdo_gleP; case. - by move => [-> _]. - by move =>[_]; rewrite ym; aw => sv; case: C0_ne_C1. - by move =>[_]; rewrite ym; aw => sv; case: C0_ne_C1. + by move =>[_]; rewrite ym; aw => sv; case: C0_ne_C1. + by move =>[_]; rewrite ym; aw => sv; case: C0_ne_C1. exists a, b; split => //. rewrite sr in asr bsr csr. rewrite ic (LfV ta asr) (LfV ta bsr)(LfV ta csr). rewrite -/c; Ytac0; Ytac0; Ytac0. rewrite inf_comparable1; [fprops | fprops | order_tac; rewrite sr'; fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)