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