proposition: Lemma length_R2 : forall t : nat, t <= size -> lengthbv (R2 t) = size.
proof: Proof. simple induction t. simpl in |- *. unfold lengthbv, BV_null in |- *. rewrite (length_list_const bool). trivial with arith. unfold lengthbv in |- *. intros. rewrite R2_eq2. rewrite (length_app bool). unfold Mux, consbv. rewrite (F_If BV BV _ _ _ highs). rewrite (F_If BV nat _ _ _ (@length bool)). rewrite highs_is_strip. rewrite (length_strip bool). rewrite length_BV_full_adder_sum. unfold lengthbv in |- *. rewrite H. rewrite highs_is_strip. rewrite (length_strip bool). rewrite H. rewrite If_eq. rewrite (F_If BV nat _ _ _ (@length bool)). simpl in |- *. rewrite If_eq. symmetry in |- *. rewrite plus_comm. apply le_plus_minus. auto with arith. auto with arith. rewrite H. auto with arith. apply le_Sn_le; exact H0. apply le_Sn_le; exact H0. unfold lengthbv in |- *. rewrite H. auto with arith. apply le_Sn_le; exact H0. rewrite length_BV_full_adder_sum. unfold lengthbv in |- *. rewrite H. auto with arith. apply le_Sn_le; exact H0. unfold lengthbv in |- *. rewrite H. auto with arith. apply le_Sn_le; exact H0. Qed.
imports: BV Adder Gt