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