proposition: Lemma Exercise1_10_bis (r := order_product2 Nat_order Nat_order) (r':= Nat_order) (f := Lf (fun z => (P z) +c (Q z)) (Nat \times Nat) Nat): Exercise1_10_counterexample r r' f.
proof: Proof. move:Nat_order_wor=> [pa sr']. have l1: lattice Nat_order by apply: total_order_lattice;apply: worder_total. have l2: lattice r by apply: product2_lattice. move: (l1)(l2) => [or1 _][or2 _]. have sr: substrate r = Nat \times Nat. by rewrite order_product2_sr// -/r' sr'. rewrite /f - sr. have ta: lf_axiom (fun z => (P z) +c (Q z)) (substrate r) Nat. by rewrite sr;move => z /setX_P [_ p1 p2]; apply: NS_sum. have fp: function_prop (Lf (fun z => P z +c Q z) (substrate r) Nat) (substrate r) (substrate r') by split;aw => //;apply: lf_function. split => //. split => // x y. move /order_product2_P; rewrite -/r' sr' - sr; move=> [xp yp [le1 le2]]. rewrite LfV // LfV //. move: le1 le2 => /Nat_order_leP [p1 p2 p3] /Nat_order_leP [p4 p5 p6]. by apply /Nat_order_leP;split => //; fprops; apply: csum_Mlele. set a := (J \1c \0c); set b:= (J \0c \1c). move: NS0 NS1; rewrite /natp => ns0 ns1. have asr: inc a (substrate r) by rewrite sr /a; fprops. have bsr: inc b (substrate r) by rewrite sr /b; fprops. move: (lattice_inf_pr l2 asr bsr). set c:= inf r a b. move => [] /order_product2_P [csr _ []] _ /Nat_order_leP [_ _ p1]. move => /order_product2_P [_ _ []] /Nat_order_leP [_ _ p2] _ h. have: c = J (P c) (Q c) by aw; move: csr => /setX_P []. move: p1 p2; rewrite /a /b; aw => p1 p2. rewrite (cle0 p1) (cle0 p2) => cv. rewrite sr' - sr in csr. exists a, b; split => //; rewrite (LfV ta csr) cv. rewrite (LfV ta asr) (LfV ta bsr) !pr1_pair ! pr2_pair. rewrite (csum0r CS0) (csum0r CS1) (csum0l CS1). have osr: inc \1c (substrate r') by rewrite sr'; fprops. by rewrite inf_comparable1 //; [fprops | order_tac]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)