proposition: Lemma a_very_specific_lemma1 : forall a b c d e f : Z, c <> 0%Z -> (a * b)%Z = (c * d)%Z -> (c * e)%Z = (f * b)%Z -> (a * e)%Z = (f * d)%Z.
proof: Proof. intros. cut ((a * (c * e))%Z = (a * (f * b))%Z). intro. cut ((f * (a * b))%Z = (f * (c * d))%Z). intro. cut ((a * (f * b))%Z = (f * (a * b))%Z). intro. cut ((a * (c * e))%Z = (f * (a * b))%Z). intro. cut ((a * (c * e))%Z = (f * (c * d))%Z). intro. cut ((a * (c * e))%Z = (c * (a * e))%Z). intro. cut ((f * (c * d))%Z = (c * (f * d))%Z). intro. cut ((c * (a * e))%Z = (a * (c * e))%Z). intro. cut ((c * (a * e))%Z = (f * (c * d))%Z). intro. cut ((c * (a * e))%Z = (c * (f * d))%Z). intro. exact (Zmult_absorb c (a * e) (f * d) H H11). cut ((f * (c * d))%Z = (c * (f * d))%Z). intro. exact (trans_eq H10 H11). exact (Zmult_permute f c d). exact (trans_eq H9 H6). exact (Zmult_permute c a e). exact (Zmult_permute f c d). exact (Zmult_permute a c e). exact (trans_eq H5 H3). exact (trans_eq H2 H4). exact (Zmult_permute a f b). cut (f = f). intro. exact (f_equal2 Zmult H3 H0). trivial. cut (a = a). intro. exact (f_equal2 Zmult H2 H1). trivial. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid