proposition: Theorem lit_insert_ordered: forall c l, ordered_clause c -> ordered_clause (lit_insert l c).
proof: Proof. unfold ordered_clause, lit_insert; intros c l H; apply insert_olist; auto. exact lit_test_trans. intros; apply lit_test_anti_sym. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia