proposition: Lemma add_normal a: T3nf a -> normal (T3add a).
proof: Proof. move => na;split. by move => x nx; apply: nf_add. by move => x y nx ny; rewrite T3lt_add2l. move => x nx lx; split. by apply: nf_add. by move => y _ /T3ltW; rewrite T3le_add2l. move => z nz zp; case (T3ltP z a) => az. by exists zero; move: lx;rewrite T3addn0 az T3lt0n; case x. move: (sub_pr1 nz az) => sa. move:zp; rewrite {1} sa T3lt_add2l => sb. exists (T3succ (z - a)). by rewrite (nf_succ (nf_sub nz na)) (limit_pr lx sb) {1} sa T3lt_add2l succ_lt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)