proposition: Lemma sub_pr1 a b: T2nf b -> a <= b -> b = a + (b - a).
proof: Proof. move => nb; rewrite /T2le. case: (altP (a =P b)) => [-> | _ /=]; first by rewrite T2ltnn T2subnn T2addn0. move: nb; elim: a b; first by move => b nb; rewrite T2subn0 //. move => a' _ b' _ n' c' Hc; case; [by rewrite T2ltn0 | move => a b n c]. have aux: (n' < n)%N ->n = (n' + (n - n').-1).+1. by move => le1; rewrite - {1} (subnKC le1) subnS addSn. move => sa sb;rewrite /= (T2lt_anti sb). move: sb; rewrite T2lt_consE - T2lt_psi. have ->:(a' == a) && (b' == b) = ( [a', b'] == [a, b]) by rewrite T2eqE !andbT. case: (T2ltgtP [a', b'] [a, b]) => sb; rewrite ? sb //. move: sa; case: sb => <- <- => sa. have sb: [a', b'] = one -> c = zero. by move => h;move: sa;case:h => -> -> /= /andP[_];rewrite T2lt1 => /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 T2ltnn - hh sb | rewrite !T2ltnn - hh ]. move => dd'; case: eqP; first by move => h; move: dd';rewrite (sb h) T2ltn0. move: sa => /and4P [_ _ nd ne] _; move: (Hc c nd dd') => h. have: c - c' < [a', b'] by move: (T2le_lt_trans (sub_le1 c' nd) ne). rewrite - h; move: dd'; rewrite {1} h;case: (c - c'). by rewrite T2addn0 T2ltnn. move => a1 b1 c1 n1 d1. rewrite T2lt_consE T2ltn0 ltn0 !if_same if_simpl -T2lt_psi=> ha. by rewrite ha (T2lt_anti ha). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)