proposition: Lemma sub_pr1 a b: T1nf b -> a <= b -> b = a + (b - a).
proof: Proof. move => nb; rewrite /T1le. case: (altP (a =P b)) => [-> | _ /=]; first by rewrite T1subnn T1addn0. move: nb; elim: a b; first by move => b nb; rewrite T1sub0 //. move => a' _ n' b' Hb; case; [by rewrite T1ltn0 | move => a n b]. case: a; [ move => hb hc | move => a'' n'' b'']. move: hb hc => /=;rewrite T1lt1 => /andP [_ /eqP ->]. case a'=> //; rewrite !T1ltn0 eqxx if_same if_simpl => le1. by rewrite (ltnNge) (ltnW le1) (gtn_eqF le1) /= - addSn - subnS (subnKC le1). move => /and3P [_ sb sc]. move: (Hb _ sb) (T1le_lt_trans (sub_le1 b' sb) sc) => ha hb /=. case (T1ltgtP a' (cons a'' n'' b'')) => //. case a' => // a3 n3 b3 /=; rewrite T1eqE (eq_sym a'' a3) (eq_sym n'' n3). case (T1ltgtP a3 a'') => //= pa; first by rewrite pa. case (ltngtP n3 n'') => //= pb; first by rewrite pa T1ltnn eqxx pb. by move => h; rewrite (T1lt_anti h) (T1lt_ne' h) pa pb T1ltnn ltnn ! eqxx h. move ->;rewrite !T1ltnn ltnn !eqxx (eq_sym n n');case (ltngtP n' n) => //. by rewrite T1ltnn => le1; rewrite - addSn - subnS (subnKC le1). move => -> hw; rewrite (T1lt_anti hw); move: (ha hw) hb; clear hw. case (b - b'); first by rewrite T1addn0 => ->. by move => u v w; rewrite phi0_lt1 => <- ua; rewrite ua (T1lt_anti ua). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)