proposition: Lemma ltBleB_adcB n : forall c (p1 p2 p : BITS n), splitmsb (adcBmain c p1 p2) = (false,p) -> if c then ltB p1 p else leB p1 p.
proof: Proof. induction n. + move => c p1 p2 p H. rewrite (tuple0 p) (tuple0 p1). destruct c. simpl in H. inversion H. done. + move => c. case/tupleP => [b1 p1]. case/tupleP => [b2 p2]. case/tupleP => [b p]. simpl. rewrite !theadCons !beheadCons. destruct c. move => H. simpl in H. destruct b1. specialize (IHn true p1 p2). case E: (splitmsb (adcBmain true p1 p2)) => [carry' p']. destruct b2. rewrite beheadCons theadCons E in H. inversion H. rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite IHn; first by rewrite orTb. done. rewrite beheadCons E in H. inversion H. rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite IHn; first by rewrite orTb. done. destruct b2. specialize (IHn true p1 p2). case E: (splitmsb (adcBmain true p1 p2)) => [carry' p']. rewrite beheadCons E in H. inversion H. rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite IHn; first by rewrite orTb. done. specialize (IHn false p1 p2). case E: (splitmsb (adcBmain false p1 p2)) => [carry' p']. rewrite beheadCons E in H. inversion H. rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. simpl. rewrite /leB in IHn. rewrite !andbT. by rewrite IHn. move => H. simpl in H. destruct b1. destruct b2. specialize (IHn true p1 p2). case E: (splitmsb (adcBmain true p1 p2)) => [carry' p']. rewrite beheadCons E in H. inversion H. rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. specialize (IHn _ E). rewrite /leB. simpl. rewrite !beheadCons. by rewrite IHn. specialize (IHn false p1 p2). case E: (splitmsb (adcBmain false p1 p2)) => [carry' p']. rewrite beheadCons E in H. inversion H. rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite /leB. simpl. rewrite !beheadCons. specialize (IHn _ E). rewrite /leB in IHn. rewrite andbF. rewrite orbF. done. specialize (IHn false p1 p2). destruct b2. case E: (splitmsb (adcBmain false p1 p2)) => [carry' p']. rewrite beheadCons E in H. inversion H. rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite /leB. simpl. rewrite !beheadCons !theadCons. rewrite /leB in IHn. specialize (IHn _ E). rewrite orbA. rewrite orbF. rewrite orbA. rewrite orbF. rewrite IHn. done. case E: (splitmsb (adcBmain false p1 p2)) => [carry' p']. rewrite beheadCons E in H. inversion H. rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite /leB. simpl. rewrite !beheadCons !theadCons. specialize (IHn _ E). rewrite /leB in IHn. rewrite andbT. rewrite andbF. rewrite orbF. done. 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)