proposition: Lemma nf_Wf : well_founded_P T3nf T3lt.
proof: Proof. have az: Acc (restrict T3nf T3lt) zero by split => y [_]; rewrite T3ltn0. rewrite /well_founded_P. set r:= (restrict (fun x : T3 => T3nf x) (fun a b : T3 => a < b)). have TV: forall a b c n d, T3nf (cons a b c n d) -> Acc r [a,b,c] -> Acc r (cons a b c n d). move => a b c n d nx ay. move: (nx); rewrite nf_consE => /and3P [ny nd dy]. have aux: forall a' b' c' n' d', [a', b', c'] < [a, b, c] -> T3nf (cons a' b' c' n' d') -> Acc r (cons a' b' c' n' d'). move => a' b' c' n' d' h nx'; set x := (cons a' b' c' n' d'). have h': (x < [a, b, c]) by rewrite psi_lt1. have h'': r x [a, b, c] by split. exact: (acc_rec h'' ay). suff h: forall n, Acc r (cons a b c n zero). move: (h n.+1) => h1. have h2: (cons a b c n d) < (cons a b c n.+1 zero). by rewrite T3lt_consE !eqxx ltnS leqnn /= if_same. have h3: r (cons a b c n d) (cons a b c n.+1 zero) by []. exact: (acc_rec h3 h1). clear nx dy nd d n. elim => [// | n Hr]; split; case; first by move => _; apply:az. move => a' b' c' n' d' []; rewrite T3lt_consE. case(T3ltgtP [a', b', c'] [a, b, c]); first by move => h h' _ h''; apply: aux. done. case; move => -> -> ->; rewrite T3ltn0 if_same if_simpl ltnS leq_eqVlt. move => ta;case /orP => nn'; last first. have h': r (cons a b c n' d') (cons a b c n zero). by split => //;rewrite T3lt_consE !eqxx nn' /= if_same. move => _; exact: (acc_rec h' Hr). move: ta;rewrite (eqP nn') nf_consE => /and3P [_ nd dy]. have rd: r d' [a, b, c] by split. elim: (acc_rec rd ay) => y Ha Hb. split; case; first by move => _;apply: az. move => a'' b'' c'' n'' d'' []; rewrite T3lt_consE. case: (T3ltgtP [a'', b'', c''] [a, b, c]). by move => sa sb sc _;apply: aux. done. case => -> -> -> sa sb sc; move: sb;case: (ltngtP n'' n) => cnn dy'. have h'': r (cons a b c n'' d'') (cons a b c n zero). by split => //; rewrite T3lt_consE !eqxx T3ltnn cnn. exact: (acc_rec h'' Hr). by case dy'. move: sa sc;move/and5P => [_ _ _ ny' _] /and5P [_ _ _ nd'' _]. by rewrite cnn; apply: Hb. have TIX: forall a b c, T3nf [a,b,c] -> Acc r b -> Acc r c -> (forall a' b' c', r a' a -> Acc r b' -> Acc r c' -> T3nf b' -> T3nf c' -> Acc r [a', b', c'])-> (forall b' c', r b' b -> Acc r c'-> T3nf c' -> Acc r [a, b', c'])-> (forall c', r c' c -> Acc r [a, b, c'])-> Acc r [a,b,c]. move => a b c nanc ab ac Ha Hb Hc; split. move => y; set n := (size y).+1. move: (leqnn n); rewrite {1}/n; move: n => n. elim: n y => [ // | n Hr]; case; first by move => _ _; apply: az. move => a' b' c' n' d' ll [nu lta nv]. apply: TV; first by exact. move: (nv); rewrite nf_psi => /and3P[na nb nc]. move: nu; rewrite nf_consE => /and3P [nu _ _]. move: (nu); rewrite nf_psi => /and3P[na' nb' nc']. move: (size_prop1 a' b' c' n' d') => /and5P [_ lb lc _ _]. move:ll; rewrite ltnS => ll. move: (leq_trans lb ll)(leq_trans lc ll) => lb' lc'{lb lc}. move: lta; rewrite psi_lt1 T3lt_psi /lt_psi. case /orP; first by move /and3P => [ /eqP -> /eqP -> cc]; apply Hc. case /orP. by move /and3P => [/eqP -> lb lc];apply: Hb; [ |apply: Hr |]. case /orP; first by move /and3P => [_ _ lc]; apply: (acc_rec _ ac). case /orP; first by move /and3P => [_ _ /eqP ->]. case /orP. by move /and3P => [la lb lc] ;apply: Ha; try apply: Hr. case /orP; first by move => /andP [_ h]; exact: (acc_rec (And3 nu h nb) ab). case /orP; first by move => /andP [_ /eqP ->]. case /orP; first by move => /andP [_ h]; exact: (acc_rec (And3 nu h nc) ac). by move => /andP [_ /eqP ->]. have TX: forall a b c, T3nf [a,b,c] -> Acc r b -> Acc r c -> (forall a' b' c', r a' a -> Acc r b' -> Acc r c' -> T3nf b' -> T3nf c' -> Acc r [a', b', c']) -> (forall b' c', r b' b -> Acc r c' -> T3nf c' -> Acc r [a, b', c']) -> Acc r [a,b,c]. move => a b c nabc ab ac h1 h2. apply: (TIX _ _ _ nabc ab ac h1 h2); elim: ac => x Ha Hb c' cx. have np: T3nf [a, b, c']. have [nc' _ _] := cx. by move: nabc ; rewrite !nf_psi nc' => /and3P[-> -> _]. by apply: (TIX a b c' np ab (Ha _ cx) h1 h2)=> w rwc;apply: (Hb c' cx). have TXI: forall a b c, T3nf [a,b,c] -> Acc r b -> Acc r c -> (forall a' b' c', r a' a -> Acc r b' -> Acc r c' -> T3nf b' -> T3nf c'-> Acc r [a', b', c']) -> Acc r [a,b,c]. move => a b c nabc ab ac h1. apply: (TX _ _ _ nabc ab ac h1); elim: ab => x Ha Hb b' c' bx ac' nc'. have np: T3nf [a, b', c']. move: (bx) => [nb' _ _]. by move: nabc ; rewrite !nf_psi nb' nc' => /and3P[-> _ _]. apply: (TX a b' c' np (Ha _ bx) ac' h1) => u v uv av nv. exact: (Hb b' bx u v uv av nv). have TXII: forall a b c, T3nf [a, b, c] -> Acc r a -> Acc r b -> Acc r c -> Acc r [a, b, c]. move => a b c np aa ab ac; apply: (TXI _ _ _ np ab ac). elim: aa => x Ha Hb a' b' c' lax ab' ac' nb' nc'. have np': T3nf [a', b', c']. by move: (lax) => [na' _ _];rewrite !nf_psi na' nb' nc'. apply: (TXI a' b' c' np' ab' ac') => a'' b'' c'' r1 ab'' ac'' nb'' nc''. exact: (Hb a' lax a'' b'' c'' r1 ab'' ac'' nb'' nc''). move => a; set n := (size a).+1. move: (leqnn n); rewrite {1}/n; move: n => n. elim: n a => [ // | n Hr]; case; first by move => _ _; apply: az. move => a' b' c' n' d' ll nx. move: (nx); rewrite nf_consE =>/and3P [np _ _]. move:(np); rewrite nf_psi => /and3P[na nb nc]. move /and5P: (size_prop1 a' b' c' n' d') => [la lb lc _ _]. move: (leq_trans la ll)(leq_trans lb ll)(leq_trans lc ll) => la' lb' lc'. by apply:TV; [ exact | apply: TXII]; first (by exact); apply: Hr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)