∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).