proposition: Theorem Qbar_lt_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 a as [a| ]; [ idtac | inversion Hac ]. destruct b as [b| ]; [ idtac | inversion Hab ]. unfold Qbar.qeq in Hab. destruct d as [d| ]; [ idtac | constructor ]. apply Qbar.lt_qfin. destruct c as [c| ]; [ idtac | inversion Hcd ]. unfold Qbar.qeq in Hcd. rewrite <- Hab, <- Hcd. inversion Hac; assumption. Qed.
imports: Utf8 QArith Misc