proposition: Lemma join_together {A} {JA : Join A} {PA : Perm_alg A} {SA: Sep_alg A} {CaA : Canc_alg A} {CrA : Cross_alg A} {DA : Disj_alg A}: forall p q m n w i, join p q w -> join m n w -> join p m i -> exists j, join i j w.
proof: Proof. intros; destruct_cross w. try_join pm m pmm. try_join pm pm pmpm. apply join_self' in H8. subst. apply join_comm in H6. generalize (join_canc H9 H6); intro. subst. equate_join m pmm. apply unit_identity in H4. apply (join_unit1_e pn p H4) in H2. subst. try_join p m i'. equate_join i i'. apply join_comm in H8. exists qn. auto. Qed.
imports: VST.msl.msl_standard CertiGraph.msl_ext.ramify_tactics Coq.Sorting.Permutation