proposition: Lemma C_inv_r : forall x : Ccring, ~ Equal x (monoid_unit Ccring) -> Equal (ring_mult x (Ap Cinv_map x)) (ring_unit Ccring).
proof: Proof. intros x; try assumption. simpl in |- *. unfold Ceq in |- *; simpl in |- *. unfold field_div in |- *. elim x. intros r i; try assumption. simpl in |- *. intros H'; split; [ try assumption | idtac ]. apply Trans with (sgroup_law R (ring_mult (ring_mult r r) (field_inverse (sgroup_law R (ring_mult r r) (group_inverse R (ring_mult i (group_inverse R i)))))) (group_inverse R (ring_mult (ring_mult i (group_inverse R i)) (field_inverse (sgroup_law R (ring_mult r r) (group_inverse R (ring_mult i (group_inverse R i)))))))). auto with algebra. apply Trans with (sgroup_law (Build_field R) (ring_mult (ring_mult r r) (field_inverse (sgroup_law (Build_field R) (ring_mult r r) (group_inverse (Build_field R) (ring_mult i (group_inverse (Build_field R) i)))))) (ring_mult (group_inverse (Build_field R) (ring_mult i (group_inverse (Build_field R) i))) (field_inverse (sgroup_law (Build_field R) (ring_mult r r) (group_inverse (Build_field R) (ring_mult i (group_inverse (Build_field R) i))))))). auto with algebra. apply Trans with (ring_mult (sgroup_law (Build_field R) (ring_mult r r) (group_inverse (Build_field R) (ring_mult i (group_inverse (Build_field R) i)))) (field_inverse (sgroup_law (Build_field R) (ring_mult r r) (group_inverse (Build_field R) (ring_mult i (group_inverse (Build_field R) i)))))). auto with algebra. apply (FIELD_inverse_r (K:=R)). red in |- *. intros H'0; try assumption. cut (Equal (sgroup_law (Build_field R) (ring_mult r r) (ring_mult i i)) (monoid_unit (Build_field R))). intros H'1; try assumption. absurd (Equal r (monoid_unit R) /\ Equal i (monoid_unit R)); auto with algebra. apply Trans with (sgroup_law (Build_field R) (ring_mult r r) (group_inverse (Build_field R) (ring_mult i (group_inverse (Build_field R) i)))). apply SGROUP_comp. auto with algebra. apply Trans with (group_inverse (Build_field R) (group_inverse (Build_field R) (ring_mult i i))). auto with algebra. auto with algebra. auto with algebra. apply Trans with (sgroup_law R (ring_mult (ring_mult r (group_inverse R i)) (field_inverse (sgroup_law R (ring_mult r r) (group_inverse R (ring_mult i (group_inverse R i)))))) (ring_mult (ring_mult i r) (field_inverse (sgroup_law R (ring_mult r r) (group_inverse R (ring_mult i (group_inverse R i))))))). auto with algebra. apply Trans with (ring_mult (sgroup_law (Build_field R) (ring_mult r (group_inverse (Build_field R) i)) (ring_mult i r)) (field_inverse (sgroup_law R (ring_mult r r) (group_inverse R (ring_mult i (group_inverse R i)))))). auto with algebra. apply Trans with (ring_mult (monoid_unit R) (field_inverse (sgroup_law R (ring_mult r r) (group_inverse R (ring_mult i (group_inverse R i)))))). apply RING_comp. apply Trans with (sgroup_law (Build_field R) (group_inverse (Build_field R) (ring_mult r i)) (ring_mult i r)). auto with algebra. apply Trans with (sgroup_law (Build_field R) (group_inverse (Build_field R) (ring_mult i r)) (ring_mult i r)). auto with algebra. auto with algebra. auto with algebra. auto with algebra. Qed.
imports: Cfield_facts Ring_util