proposition: Lemma sbb0B_carry n (p: BITS n.+1) : fst (sbbB false #0 p) = (p != #0).
proof: Proof. rewrite /sbbB. simpl (~~false). rewrite /adcB. elim E: (splitmsb (adcBmain true #0 (invB p))) => [carry res]. rewrite -(toNatK (adcBmain true #0 (invB p))) in E. rewrite splitmsb_fromNat in E. rewrite toNat_adcBmain toNat_fromNat0 addn0 toNat_invB in E. inversion E. clear E H0 H1. rewrite add1n. case E: (p == #0). + rewrite (eqP E). rewrite toNat_fromNat0. rewrite subn0. rewrite prednK; last apply expn_gt0. by rewrite divnn expn_gt0. + apply negbT in E. have [m H] := (nonZeroIsSucc E). rewrite H. rewrite divn_small => //. rewrite -subSn. rewrite prednK; last apply expn_gt0. apply pow2_sub_ltn. have B:= toNatBounded p. rewrite H in B. have HH := @ltn_sub2r 1 m.+1 (2^n.+1). rewrite subn1 in HH. rewrite prednK in HH => //. rewrite subn1 in HH. apply HH. apply pow2_gt1. apply B. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)