proposition: Lemma quot_mul_cancel_r : forall a b c, b~=0 -> c~=0 -> (a*c)÷(b*c) == a÷b.
proof: Proof. assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a*c)÷(b*c) == a÷b). { intros a b c **. pos_or_neg c. - apply NZQuot.div_mul_cancel_r; order. - rewrite <- quot_opp_opp, <- 2 mul_opp_r. + apply NZQuot.div_mul_cancel_r; order. + rewrite <- neq_mul_0; intuition order. } assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a*c)÷(b*c) == a÷b). { intros a b c **. pos_or_neg b. - apply Aux1; order. - apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_l; try order. + apply Aux1; order. + rewrite <- neq_mul_0; intuition order. } intros a b c **. pos_or_neg a. { apply Aux2; order. } apply opp_inj. rewrite <- 2 quot_opp_l, <- mul_opp_l; try order. { apply Aux2; order. } rewrite <- neq_mul_0; intuition order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv