proposition: Lemma a_very_specific_lemma5' : forall (m n p : positive) (a b c : Z), (a * n < b * m)%Z -> (b * p)%Z = (c * n)%Z -> (a * p < c * m)%Z.
proof: Proof. intros. case (dec_eq b 0). intro. rewrite H1 in H0. simpl in H0. cut (c = 0%Z). intro. rewrite H2. rewrite H1 in H. simpl in H. simpl in |- *. apply Z.gt_lt. cut (a * 0 > a * p)%Z. intro. rewrite Zmult_0_r in H3. assumption. apply Zlt_conv_mult_l. apply Z.gt_lt. cut (- (0) > - - a)%Z. simpl in |- *. rewrite Z.opp_involutive. trivial. apply Zlt_opp. apply Zmult_gt_0_lt_0_reg_r with (n := n). auto with zarith. rewrite Zopp_mult_distr_l_reverse. cut (- (a * n) > - (0))%Z. simpl in |- *. intro. apply Z.gt_lt. trivial. apply Zlt_opp. assumption. apply Z.gt_lt. auto with zarith. apply Zmult_integral_l with (n := n). apply Zgt_not_eq. auto with zarith. apply sym_eq. assumption. intro. case (not_Zeq b 0 H1). intro. cut (b * p < 0)%Z. intro. cut (b * p * (a * n) > b * p * (b * m))%Z. intro. cut (b * p * (a * n) > c * n * (b * m))%Z. intro. apply Z.gt_lt. apply Zgt_mult_reg_absorb_l with (a := n). auto with zarith. apply Z.lt_gt. apply Zgt_mult_conv_absorb_l with (a := b). assumption. replace (b * (n * (a * p)))%Z with (b * p * (a * n))%Z by ring. replace (b * (n * (c * m)))%Z with (c * n * (b * m))%Z by ring; auto. rewrite <- H0. auto. apply Zlt_conv_mult_l;trivial. apply Z.gt_lt. replace 0%Z with (b * 0)%Z by ring. apply Zlt_conv_mult_l; trivial. apply Z.gt_lt. auto with zarith. intro. cut (b * p > 0)%Z. intro. cut (b * p * (a * n) < b * p * (b * m))%Z. intro. cut (b * p * (a * n) < c * n * (b * m))%Z. intro. apply Z.gt_lt. apply Zgt_mult_reg_absorb_l with (a := n). auto with zarith. apply Zgt_mult_reg_absorb_l with (a := b). apply Z.lt_gt. assumption. apply Z.lt_gt. replace (b * (n * (a * p)))%Z with (b * p * (a * n))%Z by ring. replace (b * (n * (c * m)))%Z with (c * n * (b * m))%Z by ring; auto. rewrite <- H0. auto. apply Zlt_reg_mult_l; auto. apply Zmult_gt_0_compat; auto with zarith. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid