proposition: Lemma strip_sym : forall (v : list A) (i j : nat), strip (strip v i) j = strip (strip v j) i.
proof: Proof. simple induction v. intros. rewrite strip_nil. rewrite strip_nil. trivial with arith. simple induction i. intro. rewrite strip_O. rewrite strip_O. trivial with arith. simple induction j. rewrite strip_O. rewrite strip_O. try trivial with arith. intros. rewrite strip_cons_S. rewrite strip_cons_S. replace (strip (strip l n) (S n0)) with (strip (strip l (S n)) n0). apply H. apply strip_strip_S. Qed.
imports: Arith_compl Minus Lists_compl