proposition: Theorem Qcmp_sym : ∀ a b c d, (a ?= b) = (c ?= d) → (b ?= a) = (d ?= c).
proof: Proof. intros a b c d H. remember (a ?= b) as cmp. symmetry in Heqcmp, H. destruct cmp. apply Qeq_alt in Heqcmp. apply Qeq_alt in H. rewrite Heqcmp, H. do 2 rewrite Qcmp_eq. reflexivity. apply Qcmp_lt_gt in Heqcmp. apply Qcmp_lt_gt in H. rewrite <- H in Heqcmp; assumption. apply Qcmp_gt_lt in Heqcmp. apply Qcmp_gt_lt in H. rewrite <- H in Heqcmp; assumption. Qed.
imports: Utf8 QArith Slope_base Misc