proposition: Theorem Qbar_le_compat : ∀ a b c d, (a = b)%Qbar → (c = d)%Qbar → (a ≤ c)%Qbar → (b ≤ d)%Qbar.
proof: Proof. intros a b c d Hab Hcd Hac. destruct d as [d| ]; [ idtac | constructor ]. destruct b as [b| ]. apply Qbar.le_qfin. destruct c as [c| ]; [ idtac | inversion Hcd ]. unfold Qbar.qeq in Hcd. rewrite <- Hcd. destruct a as [a| ]; [ idtac | inversion Hab ]. unfold Qbar.qeq in Hab. rewrite <- Hab. inversion Hac; assumption. destruct c as [c| ]; [ idtac | inversion Hcd ]. unfold Qbar.qeq in Hcd. destruct a as [a| ]; [ inversion Hab | inversion Hac ]. Qed.
imports: Utf8 QArith Misc