proposition: Lemma Exercise1_4c3 r r' x y: order r -> total_order r' -> substrate r = singleton x -> inc y (substrate r') -> ncr_component (order_product2 r r') (J x y) = singleton (J x y).
proof: Proof. move=> or [or' tr'] sr ysr'. set r'':= order_product2 r r'. have xsr: inc x (substrate r) by rewrite sr; fprops. have or'': order r'' by apply: order_product2_or. move: (ncr_properties or'') => [p1 p2 p3 p4]. have Jsr: inc (J x y) (substrate r'') by rewrite order_product2_sr; fprops. rewrite -(p3 _ Jsr). have lexx: gle r x x by order_tac. have pa: (substrate r \times substrate r') = substrate r''. by rewrite order_product2_sr. have xt: forall t, not_comp_rel r'' t (J x y) -> t = J x y. move => u [q1 q2 h]; case: h; first by move=> ->. move: (q1); rewrite -pa // sr; move => /setX_P [] pu /set1_P Pu Qu. case: (tr' _ _ Qu ysr'). by move=> h1 h2;case: h2; left; apply /order_product2_P; aw; rewrite pa Pu. by move=> h1 h2; case: h2; right; apply /order_product2_P; aw; rewrite pa Pu. set_extens t; last first. move /set1_P ->; apply /(class_P p1); apply: (reflexivity_e p1); ue. move /(class_P p1) => r1; apply /set1_P;move: (symmetricity_e p1 r1). move /Zo_hi; aw; move=> [c [cc <- tc]]; move: c cc tc. elim => u v; simpl; first by move => h1 h2; rewrite h2 in h1; apply: (xt _ h1). by move=> h1 [h2 h3] h4; rewrite (h1 h3 h4) in h2; apply: xt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)