proposition: Theorem clause_insert_ordered: forall c cs, ordered_clause c -> ordered cs -> ordered (clause_insert c cs).
proof: Proof. intros c cs H H1 n1 c1 H2. case (clause_insert_in (n1, c1) c cs); auto. intros tmp _; case tmp; clear tmp; auto; intros H3. injection H3; intros; subst; auto. apply (H1 n1 c1); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia