proposition: Lemma Qhomographic_sign_equal_strong : forall (a1 a2 b1 b2 c1 c2 d1 d2 : Z) (p1 p2 : Qpositive) (H_ok_1 : Qhomographic_sg_denom_nonzero c1 d1 p1) (H_ok_2 : Qhomographic_sg_denom_nonzero c2 d2 p2), a1 = a2 -> b1 = b2 -> c1 = c2 -> d1 = d2 -> p1 = p2 -> Qhomographic_sign a1 b1 c1 d1 p1 H_ok_1 = Qhomographic_sign a2 b2 c2 d2 p2 H_ok_2.
proof: Proof. abstract (intros; generalize H_ok_2; repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite <- id1; clear id1 end; intro; apply Qhomographic_sign_equal). Defined.
imports: Coq(ZArithRing)