proposition: Lemma double_split L R U D : L + R =mul= U + D -> R =mul= (R # D) + (U - L).
proof: Proof. intros; try_solve_meq. assert (((x/L)%msets + (x/R)%msets)%nat = ((x/U)%msets + (x/D)%msets)%nat). rewrite <- (union_mult L R). rewrite <- (union_mult U D). auto with multisets. case (Compare_dec.le_lt_dec (x/L)%msets (x/U)%msets); intro l_u. assert ((x/R)%msets >= (x/D)%msets); [lia | idtac]. rewrite (Nat.min_r (x/R)%msets (x/D)%msets); lia. assert ((x/R)%msets < (x/D)%msets); [lia | idtac]. rewrite (proj2 (Nat.sub_0_le _ _)). rewrite (Nat.min_l (x/R)%msets (x/D)%msets); lia. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)