proposition: Lemma adcB_leB_op n : forall (p1 p2 p: BITS n) c carry, splitmsb (adcBmain c p1 p2) = (carry,p) -> (if c then ltB p1 p else leB p1 p) -> carry = false.
proof: Proof. induction n. + move => p1 p2 p. rewrite (tuple0 p1) (tuple0 p2) (tuple0 p) /= => c carry. destruct c. congruence. rewrite theadCons/=. congruence. + case/tupleP => [b1 p1]. case/tupleP => [b2 p2]. case/tupleP => [b p]. move => c carry. rewrite/leB/= !beheadCons!theadCons. move => EQ PE. destruct c. rewrite /= in EQ. destruct b1. destruct b2. case E: (splitmsb (adcBmain true p1 p2)) => [carry'' p']. specialize (IHn _ _ _ _ _ E). rewrite beheadCons E in EQ. injection EQ => /val_inj E1 E2 E3. rewrite -E3. apply IHn. by rewrite /= -E1 andbF andFb orbF in PE. case E: (splitmsb (adcBmain true p1 p2)) => [carry'' p']. specialize (IHn _ _ _ _ _ E). rewrite beheadCons E in EQ. injection EQ => /val_inj E1 E2 E3. rewrite -E3. apply IHn. by rewrite -E1 andbF andFb orbF in PE. destruct b2. case E: (splitmsb (adcBmain true p1 p2)) => [carry'' p']. specialize (IHn _ _ _ _ _ E). rewrite beheadCons E in EQ. injection EQ => /val_inj E1 E2 E3. rewrite -E3. apply IHn. by rewrite /= -E1 -E2 andbF orbF in PE. case E: (splitmsb (adcBmain false p1 p2)) => [carry'' p']. specialize (IHn _ _ _ _ _ E). rewrite beheadCons E in EQ. injection EQ => /val_inj E1 E2 E3. rewrite -E3. apply IHn. by rewrite -E1 -E2 !andbT in PE. rewrite /= in EQ. destruct b1. destruct b2. case E: (splitmsb (adcBmain true p1 p2)) => [carry'' p']. specialize (IHn _ _ _ _ _ E). rewrite beheadCons E in EQ. injection EQ => /val_inj E1 E2 E3. rewrite -E3. apply IHn. by rewrite /= -E1 -E2!andbF orbF/= orbF in PE. case E: (splitmsb (adcBmain false p1 p2)) => [carry'' p']. specialize (IHn _ _ _ _ _ E). rewrite beheadCons E in EQ. injection EQ => /val_inj E1 E2 E3. rewrite -E3. apply IHn. by rewrite -E1 -E2 /= andbF andbT orbF /= in PE. destruct b2. case E: (splitmsb (adcBmain false p1 p2)) => [carry'' p']. specialize (IHn _ _ _ _ _ E). rewrite beheadCons E in EQ. injection EQ => /val_inj E1 E2 E3. rewrite -E3. apply IHn. by rewrite /= -E1 -E2 !andbT /= orbF in PE. case E: (splitmsb (adcBmain false p1 p2)) => [carry'' p']. specialize (IHn _ _ _ _ _ E). rewrite beheadCons E in EQ. injection EQ => /val_inj E1 E2 E3. rewrite -E3. apply IHn. by rewrite -E1 -E2 !andbT andbF orbF in PE. 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)