proposition: Theorem stalmarckMonotoneEx : forall (S1 S2 S3 : State) (L : list triplet), stalmarckP S1 L S3 -> inclState S1 S2 -> exists S4 : State, stalmarckP S2 L S4 /\ inclState S3 S4.
proof: Proof. intros S1 S2 S3 L H'; generalize S2; Elimc H'; auto with stalmarck; clear L S1 S2 S3. intros S1 S3 L H' S2 H'0. elim (doTripletsMonotoneEx S1 S2 S3 L); [ intros S4 E; Elimc E; intros H'7 H'8 | idtac | idtac ]; auto with stalmarck. exists S4; split; auto with stalmarck. intros a b S1 S2 S3 S4 L H' H'0 H'1 H'2 H'3 S0 H'4. elim (H'0 (addEq (a, b) S0)); [ intros S5 E; Elimc E; intros H'7 H'8 | idtac ]; auto with stalmarck. elim (H'2 (addEq (a, rZComp b) S0)); [ intros S6 E; Elimc E; intros H'9 H'10 | idtac ]; auto with stalmarck. exists (interState S5 S6); split; auto with stalmarck. apply stalmarckPSplit with (1 := H'7) (2 := H'9); auto with stalmarck. apply inclStateEqStateComp with (S1 := interState S2 S3) (S3 := interState S5 S6); auto with stalmarck. apply interMemMin; auto with stalmarck. apply inclStateTrans with (S2 := S2); auto with stalmarck. apply inclStateTrans with (S2 := S3); auto with stalmarck. intros S1 S2 S3 L H' H'0 H'1 H'2 S4 H'3. elim (H'0 S4); [ intros S6 E; elim E; intros H'6 H'7; clear E | idtac ]; auto with stalmarck. elim (H'2 S6); [ intros S7 E; elim E; intros H'8 H'9; clear E | idtac ]; auto with stalmarck. exists S7; split; auto with stalmarck. apply stalmarckTrans with (S2 := S6); auto with stalmarck. Qed.