proposition: Lemma lplus_in_elim : forall I J z, low I <= [1-]up J -> Iin z (Iplus I J) -> exc (fun x => Iin x I /\ exc (fun y => Iin y J /\ z==x+y)).
proof: Proof. intros I J z H (H1,H2); simpl in H1,H2; intros. assert (low I <= z). apply Ole_trans with (low I + low J); auto. apply (Ule_total (z-low I) (up J)); intros. apply class_exc. apply exc_intro with (low I); split; auto. apply exc_intro with (z-low I); split; auto. assert (low I <= [1-]low J). apply Ole_trans with ([1-]up J); auto. split; auto. apply Uplus_le_perm_right; auto. rewrite Uplus_sym; auto. assert (up J <= z); auto. apply Ole_trans with (z - low I); auto. apply exc_intro with (z-up J); split; auto. split; auto. apply Uplus_le_perm_left; auto. rewrite Uplus_sym; auto. apply exc_intro with (up J); auto. Qed.
imports: ALEA(Utheory)