proposition: Theorem get_mk_0: forall n p, get p (mk_0 out n) = out.
proof: Proof. intros n; elim n; unfold get; simpl; auto. intros p; case (pos2n p); auto. intros n1 Rec p; case p; simpl. intros x y; case y. case x; auto. intros x1; rewrite Nat.add_0_r. case_eq size. intros _ ; rewrite Nat.mul_0_r; auto. intros n2 Hn2. replace (S x1 * S n2) with (S (x1 * size + n2)); simpl. generalize (Rec (Pos x1 n2)); auto. rewrite Hn2; simpl; rewrite (Nat.add_comm n2); auto. intros y1; generalize (Rec (Pos x y1)); simpl; auto. rewrite <- plus_n_Sm; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia