proposition: Lemma cardinal_subset : forall s1 s2, subset s1 s2 -> cardinal s1 <= cardinal s2.
proof: Proof. intros [l1 wr1]; induction l1 as [ | e le]; intros s2 H; unfold cardinal; simpl. apply Nat.le_0_l. assert (In_e_s2 : In e s2.(support)). apply H; left; trivial. generalize (split_list_app_cons eq_elt_dec _ _ In_e_s2). destruct (split_list eq_elt_dec (support s2) e) as [l2' l2'']; clear In_e_s2; destruct s2 as [ l2 wr2]; simpl; intro; subst l2. rewrite list_app_length; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; rewrite <- list_app_length; apply le_n_S. assert (wr1' := without_red_remove e nil le wr1); simpl in wr1'. assert (wr2' := without_red_remove e l2' l2'' wr2). assert (H' : subset (mk_set le wr1') (mk_set (l2' ++ l2'') wr2')). unfold subset; simpl; intros x in_x. assert (x_diff_e : x <> e). intro x_eq_e; subst x; generalize wr1; simpl; case (In_dec eq_elt_dec e le); intros; contradiction. generalize (H x); simpl; intro H'; generalize (H' (or_intror _ in_x)); clear H'; intro H'; generalize (in_app_or _ _ _ H'); clear H'; intros [ H' | [e_eq_x | H']]; unfold mem; simpl; apply in_or_app. left; trivial. absurd (x = e); trivial; apply sym_eq; trivial. right; trivial. generalize (IHle wr1' _ H'); unfold cardinal; simpl; trivial. Qed.
imports: Coq(List Arith Lia) hydras(more_list list_permut)