proposition: Lemma exercise6_11b3 E X: exercise6_11b_assumption X E -> let R := exercise6_11b_rel X in forall x y z t, x <> y -> x<>z -> x <> t -> y <> z -> y <> t -> z <> t -> R x y -> R x z -> R x t -> R y z -> R y t -> R z t.
proof: Proof. move=> [uX alne i2 i3] R x y z t nxy nxz nxt nyz nyt nzt [XY [XYX xXY yXY]] [XZ [XZX xXZ zXZ]] [XT [XTX xXT tXT]] [YZ [YZX yYZ zYZ]] [YT [YTX yYT tYT]]. case: (equal_or_not XZ XT) => XZXT; first by exists XT; split => //; ue. case: (equal_or_not XZ YT) => XZYT; first by exists XZ; split => //; ue. case: (equal_or_not YZ XT) => YZXT; first by exists XT; split => //; ue. case: (equal_or_not YZ YT) => YZYT; first by exists YT; split => //; ue. have iXZXT: (XZ \cap XT = singleton x). by apply: set1_pr2; [ fprops | case: (i2 _ _ XZX XTX)]. have iYZYT: (YZ \cap YT = singleton y). by apply: set1_pr2; [ fprops | case: (i2 _ _ YZX YTX) ]. case: (equal_or_not XY XZ)=> XYXZ. have XYYZ: XY= YZ. have yp1:inc y (XY \cap YZ) by fprops. have zp1:inc z (XY \cap YZ) by rewrite XYXZ; fprops. case: (i2 _ _ XYX YZX) =>// h; case: nyz;apply: (h _ _ yp1 zp1). case: (equal_or_not XY YT)=> XYYT; first by exists XY; aw; split => //; ue. case: (equal_or_not XT YT) => XTYT. have xp: inc x (XY \cap YT) by aw; ue. have yp: inc y (XY \cap YT) by aw; ue. case (i2 _ _ XYX YTX) =>// h. case: nxy;apply: (h _ _ xp yp). case: (i3 _ _ _ XYX XTX YTX); first by move=> h;exists XY; split => //; ue. case; first by move=> h. case; first by move=> h. case; first by move=> h;empty_tac1 x; aw. case; first by rewrite XYYZ; move=> h; empty_tac1 y; aw. case; first by move=> h; empty_tac1 t; aw. move=> [r1 r2]. have : inc t (XT \cap YT) by fprops. by rewrite -r2 XYYZ;move /setI2_P=> [tp _]; exists YZ. have iXYXZ: (XY \cap XZ = singleton x). by apply: set1_pr2; fprops; case: (i2 _ _ XYX XZX). case:(equal_or_not XZ YZ)=> XZYZ. have : inc y (singleton x) by rewrite - iXYXZ; apply/setI2_P; split => //; ue. move/set1_P => h; case: nxy =>//. have iXZYZ: (XZ \cap YZ = singleton z). apply: set1_pr2; fprops; case (i2 _ _ XZX YZX) => //. case: (equal_or_not XY YT)=> XYYT. have XYXY: (XY = XT). have xp: inc x (XY \cap XT) by fprops. have tp: inc t (XY \cap XT) by rewrite XYYT; fprops. case (i2 _ _ XYX XTX) =>// h; case: nxt;apply: (h _ _ xp tp). case: (equal_or_not XY YZ)=> XYYZ; first by exists XY;split => //; ue. case: (i3 _ _ _ XYX XZX YZX); first by move=> h;exists XY. case; first by move=> h. case; first by move=> h. case; first by move=> h;empty_tac1 x; aw. case; first by move=> h; empty_tac1 y; aw. case; first by move=> h; empty_tac1 z; aw. move=> [r1 r2]. have : inc z (XZ \cap YZ) by fprops. rewrite -r2 XYYT;move /setI2_P=> [tp _]; exists YT; by aw. have iXYYT: (XY \cap YT = singleton y). by apply: set1_pr2; fprops; case: (i2 _ _ XYX YTX). case: (equal_or_not XT YT)=> XTYT. have : inc x (singleton y) by rewrite -iXYYT; apply/setI2_P; split => //; ue. move/set1_P => h; case: nxy =>//. have iXTYT: (XT \cap YT = singleton t). by apply:set1_pr2;fprops;case: (i2 _ _ XTX YTX). case (equal_or_not XY XT)=> XYXT. case: (equal_or_not XY YZ)=> XYYZ; first by case: YZXT; ue. case: (i3 _ _ _ XYX XZX YZX); first by move=> h. case; first by move=> h. case; first by move=> h. case; first by move=> h;empty_tac1 x; aw. case; first by move=> h;empty_tac1 y; aw. case; first by move=> h;empty_tac1 z; aw. rewrite iXYXZ iXZYZ; move=> [_ sxz]. by case: nxz; apply: set1_inj. case: (i3 _ _ _ XYX XTX YTX); first by move=> h. case; first by move=> h. case; first by move=> h. case; first by move=> h;empty_tac1 x; aw. case; first by move=> h;empty_tac1 y; aw. case; first by move=> h;empty_tac1 t; aw. rewrite iXYYT iXTYT; move=> [sy st]. by rewrite sy in st; case: nyt; apply: set1_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)