proposition: Lemma lem_le_minus_v1_Sn : forall n : nat, S n <= size -> n <= size -> size - S n <= lengthbv (appbv (highs (R1 n)) (consbv (lowbit (R2 n)) nilbv)).
proof: Proof. intros. rewrite (length_app bool). rewrite highs_is_strip. rewrite (length_strip bool). rewrite length_R1. simpl in |- *. rewrite plus_comm. rewrite <- le_plus_minus. apply minus_le_lem2. exact le_SO_size. exact H0. rewrite length_R1. exact le_SO_size. exact H0. Qed.
imports: Definitions