(a c: F) b d : a * d.1 = c * b.1 <-> a // b = c // d. Proof. split; intro E. - rewrite <-(mult_1_l (a // b)), <- (recip_inverse d), (commutativity (f:=mult) d.1 (// d)), <-simple_associativity, (simple_associativity d.1), (commutativity (f:=mult) d.1 a), E, <-simple_associativity, simple_associativity, recip_inverse, mult_1_r. apply commutativity. - rewrite <-(mult_1_r (a * d.1)), <- (recip_inverse b), <-simple_associativity, (commutativity (f:=mult) b.1 (// b)), (simple_associativity d.1), (commutativity (f:=mult) d.1), !simple_associativity, E, <-(simple_associativity c), (commutativity (f:=mult) (// d)), recip_inverse, mult_1_r. reflexivity. Qed.
Require Import