proposition: Corollary sbbB_ltB_leB n (p1 p2: BITS n) : if (sbbB false p1 p2).1 then ltB p1 p2 else leB p2 p1.
proof: Proof. rewrite /sbbB/adcB adcBmain_nat toNat_invB splitmsb_fromNat ltB_nat leB_nat. simpl. rewrite !add1n. assert (POS: 2^n > 0) by apply expn_gt0. assert (B1 := toNatBounded p1). assert (B2 := toNatBounded p2). rewrite addnBA. rewrite -subn1. rewrite addnBA; last done. rewrite -addn1. rewrite -addnAC. rewrite addn1 subn1/=. rewrite addnC. rewrite addn1. case P: (toNat p1 < toNat p2). assert (2^n + toNat p1 - toNat p2 < 2^n). rewrite -(ltn_add2r (toNat p2)). rewrite subnK. by rewrite ltn_add2l. assert (H: 2^n <= 2^n + toNat p1) by apply leq_addr. apply: leq_trans H. apply (ltnW B2). rewrite (divn_small H). done. apply negbT in P. rewrite -leqNgt in P. rewrite -(addnBA _ P) divnDl; last done. rewrite divnn POS oddD/=. rewrite negbK. assert (toNat p1 - toNat p2 < 2^n). assert (H := leq_subr (toNat p2) (toNat p1)). apply: leq_ltn_trans . apply H. done. rewrite (divn_small H). done. rewrite -(leq_add2r 1). rewrite !addn1 prednK. done. apply expn_gt0. 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)