proposition: Lemma leqt_cfun m (c : connector m) : ctransp c -> {homo (cfun c : m.-tuple A -> m.-tuple A) : i j / leqt i j}.
proof: Proof. move=> /ctranspP [cTl cTf] t1 t2 /leqtP t1Lt2; apply/leqtP => a b. rewrite leq_eqVlt => /orP[/val_eqP<-//|aLb]. have b_gt0 : 0 < b by case: (nat_of_ord b) aLb. have aLLb : a <= b by apply: ltnW. rewrite !tnth_map !tnth_ord_tuple //. have [->|/eqP cD] := clink c a =P a; last case: (cTl _ cD) => cE. - rewrite !cTf leqnn !minxx. have [->|/eqP /cTl[] cE] := clink c b =P b. - by rewrite leqnn !minxx; apply/t1Lt2. - rewrite cE leqnSn. have aLc : a <= clink c b by rewrite cE -ltnS (leq_trans aLb) // ltnW. case: (ltP (tnth t1 b)) => C1. rewrite min_l; first by apply/t1Lt2/ltnW. apply/t1Lt2; last by apply: ltW. by rewrite cE leqnSn. move=> t1aLt1c. rewrite le_min !t1Lt2 => //; try by apply: ltnW. by apply: le_trans C1. have cLb : clink c b < b. by rewrite cE /=; case: (nat_of_ord b) aLb. have aLc : a <= clink c b. by rewrite -ltnS cE prednK. rewrite (leqNgt b) cLb /=. case: (ltP (tnth t1 b)) => C1. by rewrite le_max =>/(t1Lt2 _ _ aLc) ->; rewrite orbT. by rewrite le_max =>/(t1Lt2 _ _ (ltnW aLb)) ->. - rewrite !cTf cE leqnSn /=. have [->|/eqP /cTl[] c1E] := clink c b =P b. - rewrite leqnn !minxx. case: (ltP (tnth t1 a)); rewrite ge_min. by move=> _ /t1Lt2-> //; apply: ltnW. move=> _ /t1Lt2-> //; first by rewrite orbT. by rewrite cE. - rewrite c1E leqnSn. case: (ltP (tnth t1 a)); rewrite !le_min. move=> t1aLt1c; rewrite min_l. move/andP => [] /t1Lt2-> // /t1Lt2 -> //. by rewrite c1E (leq_trans aLLb). apply: t1Lt2; first by rewrite cE. by apply: ltW. rewrite !ge_min => H /andP[] /t1Lt2 -> //; last by rewrite cE. move=> /t1Lt2 ->; rewrite ?orbT //. by rewrite cE c1E ltnS. have /negPf-> : ~~ (b <= clink c b). by rewrite c1E; case: (nat_of_ord b) aLb => //= n; rewrite ltnn. have [<-|/eqP aD] := a =P clink c b. by rewrite !(ge_min, le_max) !lexx !orbT. have aLb1 : a <= b.-1 by by rewrite -ltnS prednK //; case: (nat_of_ord b) aLb. rewrite !(ge_min, le_max) -orbA => /or4P[] /t1Lt2->//; rewrite ?(orbT, cE, c1E) //. by rewrite ltn_neqAle -c1E aD c1E. rewrite leqNgt ltn_neqAle cD cE leq_pred !cTf /=. have [->|/eqP /cTl[] c1E] := clink c b =P b. - rewrite leqnn !minxx. case: (ltP (tnth t1 a)); rewrite ge_max. move=> t1aLt1c t1cLtb; rewrite !t1Lt2 //. by rewrite cE (leq_trans (leq_pred _)). by apply: le_trans (ltW t1aLt1c) _. move=> t1aLt1c t1cLtb. have t2aLt2b : (tnth t2 a <= tnth t2 b)%O by apply: t1Lt2. rewrite t2aLt2b (le_trans _ t2aLt2b) // t1Lt2 //. by rewrite cE leq_pred. - rewrite c1E leqnSn !ge_max !le_min -!andbA => /and4P[t1aLtb t1aLt1c t1cLtb t1cLt1c]. by rewrite !t1Lt2 ?(cE, c1E, (leq_trans (leq_pred _))) // ltnW. have /negPf-> : ~~ (b <= clink c b). by rewrite c1E; case: (nat_of_ord b) aLb => //= n; rewrite ltnn. rewrite !(ge_max, le_max) => /andP[] /orP[] /t1Lt2-> //=; last first. - by rewrite c1E -ltnS prednK. - rewrite !orbT /=; case/orP => /t1Lt2-> //; rewrite ?orbT //. by rewrite cE (leq_trans (leq_pred _)). by rewrite cE c1E (leq_trans (leq_pred _)) // -ltnS prednK. case/orP => /t1Lt2-> //; rewrite ?orbT //. by rewrite cE (leq_trans (leq_pred _)). rewrite cE c1E -ltnS !prednK //. move/eqP/val_eqP: cD => /=. by rewrite /= cE; case: nat_of_ord. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple