proposition: Lemma cardinal_union: forall s1 s2, cardinal (union s1 s2) = cardinal s1 + cardinal s2 -cardinal (inter s1 s2).
proof: Proof. intros s1 s2; assert (H := cardinal_union_inter_12 s1 s2). symmetry;apply Nat.add_sub_eq_l. rewrite <- H; now rewrite Nat.add_comm. Qed.
imports: Coq(List Arith Lia) hydras(more_list list_permut)