proposition: Corollary ltB_joinmsb0_adcB n : forall p1 p2: BITS n, ltB (joinmsb0 p1) (adcBmain true p1 p2).
proof: Proof. apply (ltBleB_joinmsb0_adcB true). 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)