proposition: Theorem lit_rm_ordered: forall c1 c2, ordered_clause c1 -> ordered_clause c2 -> ordered_clause (lit_rm c1 c2).
proof: Proof. unfold ordered_clause, lit_rm; intros c1 c2 H H1; apply rm_olist; auto. exact lit_test_trans. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia