proposition: Lemma incr_decomp : forall f g: fmon natO U, orc (forall n, exc (fun m => (n<=m)%nat /\ f n <= g m)) (forall n, exc (fun m => (n<=m)%nat /\ g n <= f m)).
proof: Proof. intros f g; apply orc_intro; intros. apply H; clear H; intros. apply exc_intro_class; intros. apply H0; clear H0; intros. apply exc_intro_class; intros. case (dec_le n n0); intro. apply (incr_decomp_aux f g) with (n1:=n) (n2:=n0); auto. apply (incr_decomp_aux g f) with (n1:=n0) (n2:=n); auto; lia. Qed.
imports: ALEA(Utheory)