proposition: Lemma quadro_leq_inf : forall a b c d : Z, {(c <= a)%Z /\ (d <= b)%Z} + {~ ((c <= a)%Z /\ (d <= b)%Z)}.
proof: Proof. intros. case (Z_lt_le_dec a c). intro z. right. intro. elim H. intros. generalize z. apply Zle_not_lt. assumption. intro. case (Z_lt_le_dec b d). intro z0. right. intro. elim H. intros. generalize z0. apply Zle_not_lt. assumption. intro. left. split. assumption. assumption. Qed.
imports: Coq(Lia)