proposition: Lemma map2_or_nth_bitOf: forall (a b: list bool) (i: nat), (length a) = (length b) -> (i <= (length a))%nat -> nth i (map2 orb a b) false = (nth i a false) || (nth i b false).
proof: Proof. intro a. induction a as [ | a xs IHxs]. - intros [ | b ys]. + intros i H0 H1. do 2 rewrite map2_nth_empty_false. reflexivity. + intros i H0 H1. rewrite map2_or_empty_empty2. rewrite map2_nth_empty_false. contradict H1. simpl. unfold not. intros. easy. - intros [ | b ys]. + intros i H0 H1. rewrite map2_or_empty_empty1. rewrite map2_nth_empty_false. rewrite orb_false_r. rewrite H0 in H1. contradict H1. simpl. unfold not. intros. easy. + intros i H0 H1. simpl. revert i H1. intros [ | i]; [ |intros IHi]. * simpl. auto. * apply IHxs. inversion H0; reflexivity. inversion IHi; lia. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance