proposition: Lemma sub_pr1 a b: T3nf b -> a <= b -> b = a + (b - a).
proof: Proof. move => nb; rewrite /T3le. case: (altP (a =P b)) => [-> | _ /=]; first by rewrite T3ltnn T3subnn T3addn0. move: nb; elim: a b; first by move => b nb; rewrite T3subn0 //. move => a' _ b' _ c' _ n' d' Hd; case; [by rewrite T3ltn0 | move => a b c n d]. have aux: (n' < n)%N ->n = (n' + (n - n').-1).+1. by move => le1; rewrite - {1} (subnKC le1) subnS addSn. move => sa sb;rewrite /= (T3lt_anti sb). move: sb; rewrite T3lt_consE. case: (T3ltgtP [a', b', c'] [a, b, c]) => sb; rewrite ? sb //. move: sa; case: sb => <- <- <- => sa. have sb: [a', b', c'] = one -> d = zero. by move => h;move: sa;case:h => -> -> -> /= /andP[_];rewrite T3lt1 => /eqP ->. case: (ltngtP n' n) => sc; rewrite ? sc ?eqxx //. move: sc (aux sc); case h: (n==n'); [ by rewrite (eqP h) ltnn | move => _ hh]. by case: eqP => h1 ; [ rewrite h1 T3ltnn - hh sb | rewrite !T3ltnn - hh ]. move => dd'; case: eqP; first by move => h; move: dd';rewrite (sb h) T3ltn0. move: sa => /and5P [_ _ _ nd ne] _; move: (Hd d nd dd') => h. have: d - d' < [a', b', c'] by move: (T3le_lt_trans (sub_le1 d' nd) ne). rewrite - h; move: dd'; rewrite {1} h;case: (d - d'). by rewrite T3addn0 T3ltnn. move => a1 b1 c1 n1 d1 _; rewrite psi_lt1 => ha. by rewrite ha (T3lt_anti ha). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)